mirror of
https://github.com/sharkdp/bat.git
synced 2025-11-16 14:55:56 +00: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…”.
6.3 KiB
Vendored
6.3 KiB
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
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