Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - feat: port Topology.Instances.AddCircle #3984

Closed
wants to merge 13 commits into from
Closed

[Merged by Bors] - feat: port Topology.Instances.AddCircle #3984

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
13 commits
Select commit Hold shift + click to select a range
ddac037
feat: port Topology.Instances.AddCircle
Ruben-VandeVelde May 14, 2023
8488502
Initial file copy from mathport
Ruben-VandeVelde May 14, 2023
86bbc43
automated fixes
Ruben-VandeVelde May 14, 2023
41ef1f9
Trivial fixes
Ruben-VandeVelde May 14, 2023
69954fe
Fixes
Ruben-VandeVelde May 14, 2023
de15add
coercion to add_circle from k
loefflerd May 14, 2023
9d85a44
fixes
Ruben-VandeVelde May 14, 2023
d85c4b1
fixes
Ruben-VandeVelde May 14, 2023
01a7c49
fixes
Ruben-VandeVelde May 14, 2023
b593b24
correct case and fix one error
loefflerd May 15, 2023
505e41b
fix all errors except one
loefflerd May 15, 2023
2bb444e
style lint
loefflerd May 15, 2023
c30fc99
my heart will go on....
loefflerd May 15, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions Mathlib.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2084,6 +2084,7 @@ import Mathlib.Topology.Homotopy.Contractible
import Mathlib.Topology.Homotopy.Equiv
import Mathlib.Topology.Homotopy.Path
import Mathlib.Topology.Inseparable
import Mathlib.Topology.Instances.AddCircle
import Mathlib.Topology.Instances.ENNReal
import Mathlib.Topology.Instances.EReal
import Mathlib.Topology.Instances.Int
Expand Down
8 changes: 4 additions & 4 deletions Mathlib/Algebra/CharZero/Quotient.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -53,7 +53,7 @@ theorem nsmul_mem_zmultiples_iff_exists_sub_div {r : R} {n : ℕ} (hn : n ≠ 0)

end AddSubgroup

namespace quotientAddGroup
namespace QuotientAddGroup

theorem zmultiples_zsmul_eq_zsmul_iff {ψ θ : R ⧸ AddSubgroup.zmultiples p} {z : ℤ} (hz : z ≠ 0) :
z • ψ = z • θ ↔ ∃ k : Fin z.natAbs, ψ = θ + (k : ℕ) • (p / z : R) := by
Expand All @@ -66,13 +66,13 @@ theorem zmultiples_zsmul_eq_zsmul_iff {ψ θ : R ⧸ AddSubgroup.zmultiples p} {
simp_rw [← QuotientAddGroup.mk_zsmul, ← QuotientAddGroup.mk_add,
QuotientAddGroup.eq_iff_sub_mem, ← smul_sub, ← sub_sub]
exact AddSubgroup.zsmul_mem_zmultiples_iff_exists_sub_div hz
#align quotient_add_group.zmultiples_zsmul_eq_zsmul_iff quotientAddGroup.zmultiples_zsmul_eq_zsmul_iff
#align quotient_add_group.zmultiples_zsmul_eq_zsmul_iff QuotientAddGroup.zmultiples_zsmul_eq_zsmul_iff

theorem zmultiples_nsmul_eq_nsmul_iff {ψ θ : R ⧸ AddSubgroup.zmultiples p} {n : ℕ} (hz : n ≠ 0) :
n • ψ = n • θ ↔ ∃ k : Fin n, ψ = θ + (k : ℕ) • (p / n : R) := by
rw [← coe_nat_zsmul ψ, ← coe_nat_zsmul θ,
zmultiples_zsmul_eq_zsmul_iff (Int.coe_nat_ne_zero.mpr hz), Int.cast_ofNat]
rfl
#align quotient_add_group.zmultiples_nsmul_eq_nsmul_iff quotientAddGroup.zmultiples_nsmul_eq_nsmul_iff
#align quotient_add_group.zmultiples_nsmul_eq_nsmul_iff QuotientAddGroup.zmultiples_nsmul_eq_nsmul_iff

end quotientAddGroup
end QuotientAddGroup
46 changes: 23 additions & 23 deletions Mathlib/Algebra/Order/ToIntervalMod.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -793,7 +793,7 @@ end Zero

/-- `toIcoMod` as an equiv from the quotient. -/
@[simps symm_apply]
def quotientAddGroup.equivIcoMod (a : α) : α ⧸ AddSubgroup.zmultiples p ≃ Set.Ico a (a + p) where
def QuotientAddGroup.equivIcoMod (a : α) : α ⧸ AddSubgroup.zmultiples p ≃ Set.Ico a (a + p) where
toFun b :=
⟨(toIcoMod_periodic hp a).lift b, QuotientAddGroup.induction_on' b <| toIcoMod_mem_Ico hp a⟩
invFun := (↑)
Expand All @@ -803,23 +803,23 @@ def quotientAddGroup.equivIcoMod (a : α) : α ⧸ AddSubgroup.zmultiples p ≃
dsimp
rw [QuotientAddGroup.eq_iff_sub_mem, toIcoMod_sub_self]
apply AddSubgroup.zsmul_mem_zmultiples
#align quotient_add_group.equiv_Ico_mod quotientAddGroup.equivIcoMod
#align quotient_add_group.equiv_Ico_mod QuotientAddGroup.equivIcoMod

@[simp]
theorem quotientAddGroup.equivIcoMod_coe (a b : α) :
quotientAddGroup.equivIcoMod hp a ↑b = ⟨toIcoMod hp a b, toIcoMod_mem_Ico hp a _⟩ :=
theorem QuotientAddGroup.equivIcoMod_coe (a b : α) :
QuotientAddGroup.equivIcoMod hp a ↑b = ⟨toIcoMod hp a b, toIcoMod_mem_Ico hp a _⟩ :=
rfl
#align quotient_add_group.equiv_Ico_mod_coe quotientAddGroup.equivIcoMod_coe
#align quotient_add_group.equiv_Ico_mod_coe QuotientAddGroup.equivIcoMod_coe

@[simp]
theorem quotientAddGroup.equivIcoMod_zero (a : α) :
quotientAddGroup.equivIcoMod hp a 0 = ⟨toIcoMod hp a 0, toIcoMod_mem_Ico hp a _⟩ :=
theorem QuotientAddGroup.equivIcoMod_zero (a : α) :
QuotientAddGroup.equivIcoMod hp a 0 = ⟨toIcoMod hp a 0, toIcoMod_mem_Ico hp a _⟩ :=
rfl
#align quotient_add_group.equiv_Ico_mod_zero quotientAddGroup.equivIcoMod_zero
#align quotient_add_group.equiv_Ico_mod_zero QuotientAddGroup.equivIcoMod_zero

/-- `toIocMod` as an equiv from the quotient. -/
@[simps symm_apply]
def quotientAddGroup.equivIocMod (a : α) : α ⧸ AddSubgroup.zmultiples p ≃ Set.Ioc a (a + p) where
def QuotientAddGroup.equivIocMod (a : α) : α ⧸ AddSubgroup.zmultiples p ≃ Set.Ioc a (a + p) where
toFun b :=
⟨(toIocMod_periodic hp a).lift b, QuotientAddGroup.induction_on' b <| toIocMod_mem_Ioc hp a⟩
invFun := (↑)
Expand All @@ -829,19 +829,19 @@ def quotientAddGroup.equivIocMod (a : α) : α ⧸ AddSubgroup.zmultiples p ≃
dsimp
rw [QuotientAddGroup.eq_iff_sub_mem, toIocMod_sub_self]
apply AddSubgroup.zsmul_mem_zmultiples
#align quotient_add_group.equiv_Ioc_mod quotientAddGroup.equivIocMod
#align quotient_add_group.equiv_Ioc_mod QuotientAddGroup.equivIocMod

@[simp]
theorem quotientAddGroup.equivIocMod_coe (a b : α) :
quotientAddGroup.equivIocMod hp a ↑b = ⟨toIocMod hp a b, toIocMod_mem_Ioc hp a _⟩ :=
theorem QuotientAddGroup.equivIocMod_coe (a b : α) :
QuotientAddGroup.equivIocMod hp a ↑b = ⟨toIocMod hp a b, toIocMod_mem_Ioc hp a _⟩ :=
rfl
#align quotient_add_group.equiv_Ioc_mod_coe quotientAddGroup.equivIocMod_coe
#align quotient_add_group.equiv_Ioc_mod_coe QuotientAddGroup.equivIocMod_coe

@[simp]
theorem quotientAddGroup.equivIocMod_zero (a : α) :
quotientAddGroup.equivIocMod hp a 0 = ⟨toIocMod hp a 0, toIocMod_mem_Ioc hp a _⟩ :=
theorem QuotientAddGroup.equivIocMod_zero (a : α) :
QuotientAddGroup.equivIocMod hp a 0 = ⟨toIocMod hp a 0, toIocMod_mem_Ioc hp a _⟩ :=
rfl
#align quotient_add_group.equiv_Ioc_mod_zero quotientAddGroup.equivIocMod_zero
#align quotient_add_group.equiv_Ioc_mod_zero QuotientAddGroup.equivIocMod_zero

/-!
### The circular order structure on `α ⧸ AddSubgroup.zmultiples p`
Expand Down Expand Up @@ -921,7 +921,7 @@ private theorem toIxxMod_trans {x₁ x₂ x₃ x₄ : α}
· rw [not_le] at h₁₂₃ h₂₃₄⊢
exact (h₁₂₃.2.trans_le (toIcoMod_le_toIocMod _ x₃ x₂)).trans h₂₃₄.2

namespace quotientAddGroup
namespace QuotientAddGroup

variable [hp' : Fact (0 < p)]

Expand All @@ -932,14 +932,14 @@ theorem btw_coe_iff' {x₁ x₂ x₃ : α} :
Btw.btw (x₁ : α ⧸ AddSubgroup.zmultiples p) x₂ x₃ ↔
toIcoMod hp'.out 0 (x₂ - x₁) ≤ toIocMod hp'.out 0 (x₃ - x₁) :=
Iff.rfl
#align quotient_add_group.btw_coe_iff' quotientAddGroup.btw_coe_iff'
#align quotient_add_group.btw_coe_iff' QuotientAddGroup.btw_coe_iff'

-- maybe harder to use than the primed one?
theorem btw_coe_iff {x₁ x₂ x₃ : α} :
Btw.btw (x₁ : α ⧸ AddSubgroup.zmultiples p) x₂ x₃ ↔
toIcoMod hp'.out x₁ x₂ ≤ toIocMod hp'.out x₁ x₃ :=
by rw [btw_coe_iff', toIocMod_sub_eq_sub, toIcoMod_sub_eq_sub, zero_add, sub_le_sub_iff_right]
#align quotient_add_group.btw_coe_iff quotientAddGroup.btw_coe_iff
#align quotient_add_group.btw_coe_iff QuotientAddGroup.btw_coe_iff

instance circularPreorder : CircularPreorder (α ⧸ AddSubgroup.zmultiples p) where
btw_refl x := show _ ≤ _ by simp [sub_self, hp'.out.le]
Expand All @@ -959,10 +959,10 @@ instance circularPreorder : CircularPreorder (α ⧸ AddSubgroup.zmultiples p) w
induction x₄ using QuotientAddGroup.induction_on'
simp_rw [btw_coe_iff] at h₁₂₃ h₂₃₄⊢
apply toIxxMod_trans _ h₁₂₃ h₂₃₄
#align quotient_add_group.circular_preorder quotientAddGroup.circularPreorder
#align quotient_add_group.circular_preorder QuotientAddGroup.circularPreorder

instance circularOrder : CircularOrder (α ⧸ AddSubgroup.zmultiples p) :=
{ quotientAddGroup.circularPreorder with
{ QuotientAddGroup.circularPreorder with
btw_antisymm := fun {x₁ x₂ x₃} h₁₂₃ h₃₂₁ => by
induction x₁ using QuotientAddGroup.induction_on'
induction x₂ using QuotientAddGroup.induction_on'
Expand All @@ -977,9 +977,9 @@ instance circularOrder : CircularOrder (α ⧸ AddSubgroup.zmultiples p) :=
induction x₃ using QuotientAddGroup.induction_on'
simp_rw [btw_coe_iff]
apply toIxxMod_total }
#align quotient_add_group.circular_order quotientAddGroup.circularOrder
#align quotient_add_group.circular_order QuotientAddGroup.circularOrder

end quotientAddGroup
end QuotientAddGroup

end Circular

Expand Down
Loading