mirror of
https://github.com/sharkdp/bat.git
synced 2025-08-07 15:08:56 +02:00
0918984249
Resolves #3286 1. `lean4.json` → `lean4.tmLanguage` 1. Download `vscode-lean4/syntaxes/lean4.json` from https://github.com/leanprover/vscode-lean4/pull/623 (now merged). 2. Install the VS Code extension [TextMate Languages (pedro-w)](https://marketplace.visualstudio.com/items?itemName=pedro-w.tmlanguage). 3. Open `lean4.json` in VS Code, <kbd>F1</kbd>, and “Convert to tmLanguage PLIST File”. 2. `lean4.tmLanguage` → `lean4.sublime-syntax` Open `lean4.tmLanguage` in Sublime text, “Tools → Developer → New Syntax from lean4.tmLanguage…”.
84 lines
2.6 KiB
Lean4
Vendored
84 lines
2.6 KiB
Lean4
Vendored
import MIL.Common
|
||
import Mathlib.Topology.Instances.Real.Defs
|
||
|
||
open Set Filter Topology
|
||
|
||
variable {α : Type*}
|
||
variable (s t : Set ℕ)
|
||
variable (ssubt : s ⊆ t)
|
||
variable {α : Type*} (s : Set (Set α))
|
||
-- Apostrophes are allowed in variable names
|
||
variable (f'_x x' : ℕ)
|
||
variable (bangwI' jablu'DI' QaQqu' nay' Ghay'cha' he' : ℕ)
|
||
|
||
-- In the next example we could use `tauto` in each proof instead of knowing the lemmas
|
||
example {α : Type*} (s : Set α) : Filter α :=
|
||
{ sets := { t | s ⊆ t }
|
||
univ_sets := subset_univ s
|
||
sets_of_superset := fun hU hUV ↦ Subset.trans hU hUV
|
||
inter_sets := fun hU hV ↦ subset_inter hU hV }
|
||
|
||
|
||
namespace chess.utils
|
||
|
||
section repr
|
||
|
||
@[class] structure One₂ (α : Type) where
|
||
/-- The element one -/
|
||
one : α
|
||
|
||
structure StandardTwoSimplex where
|
||
x : ℝ
|
||
y : ℝ
|
||
z : ℝ
|
||
x_nonneg : 0 ≤ x
|
||
y_nonneg : 0 ≤ y
|
||
z_nonneg : 0 ≤ z
|
||
sum_eq : x + y + z = 1
|
||
|
||
#check Pi.ringHom
|
||
#check ker_Pi_Quotient_mk
|
||
#eval 1 + 1
|
||
|
||
/-- The homomorphism from ``R ⧸ ⨅ i, I i`` to ``Π i, R ⧸ I i`` featured in the Chinese
|
||
Remainder Theorem. -/
|
||
def chineseMap (I : ι → Ideal R) : (R ⧸ ⨅ i, I i) →+* Π i, R ⧸ I i :=
|
||
Ideal.Quotient.lift (⨅ i, I i) (Pi.ringHom fun i : ι ↦ Ideal.Quotient.mk (I i))
|
||
(by simp [← RingHom.mem_ker, ker_Pi_Quotient_mk])
|
||
|
||
lemma chineseMap_mk (I : ι → Ideal R) (x : R) :
|
||
chineseMap I (Quotient.mk _ x) = fun i : ι ↦ Ideal.Quotient.mk (I i) x :=
|
||
rfl
|
||
|
||
theorem isCoprime_Inf {I : Ideal R} {J : ι → Ideal R} {s : Finset ι}
|
||
(hf : ∀ j ∈ s, IsCoprime I (J j)) : IsCoprime I (⨅ j ∈ s, J j) := by
|
||
classical
|
||
simp_rw [isCoprime_iff_add] at *
|
||
induction s using Finset.induction with
|
||
| empty =>
|
||
simp
|
||
| @insert i s _ hs =>
|
||
rw [Finset.iInf_insert, inf_comm, one_eq_top, eq_top_iff, ← one_eq_top]
|
||
set K := ⨅ j ∈ s, J j
|
||
calc
|
||
1 = I + K := (hs fun j hj ↦ hf j (Finset.mem_insert_of_mem hj)).symm
|
||
_ = I + K * (I + J i) := by rw [hf i (Finset.mem_insert_self i s), mul_one]
|
||
_ = (1 + K) * I + K * J i := by ring
|
||
_ ≤ I + K ⊓ J i := by gcongr ; apply mul_le_left ; apply mul_le_inf
|
||
|
||
|
||
class Ring₃ (R : Type) extends AddGroup₃ R, Monoid₃ R, MulZeroClass R where
|
||
/-- Multiplication is left distributive over addition -/
|
||
left_distrib : ∀ a b c : R, a * (b + c) = a * b + a * c
|
||
/-- Multiplication is right distributive over addition -/
|
||
right_distrib : ∀ a b c : R, (a + b) * c = a * c + b * c
|
||
|
||
instance {R : Type} [Ring₃ R] : AddCommGroup₃ R :=
|
||
{ Ring₃.toAddGroup₃ with
|
||
add_comm := by
|
||
sorry }
|
||
|
||
end repr
|
||
|
||
end chess.utils
|