English
There is a canonical circular order on the quotient α / zmultiples p, extending the previous circular preorder to a full circular order structure.
Русский
Существует канонический кольцевой порядок на фактор-группе α / zmultiples p, расширяющий предшествующий кольцевой предорядок до полного кольцевого порядка.
LaTeX
$$$$ \text{CircularOrder}(\alpha / \langle p \rangle) $$$$
Lean4
instance circularOrder : CircularOrder (α ⧸ AddSubgroup.zmultiples p) :=
{
QuotientAddGroup.circularPreorder with
btw_antisymm := fun {x₁ x₂ x₃} h₁₂₃ h₃₂₁ =>
by
induction x₁ using QuotientAddGroup.induction_on
induction x₂ using QuotientAddGroup.induction_on
induction x₃ using QuotientAddGroup.induction_on
rw [btw_cyclic] at h₃₂₁
simp_rw [btw_coe_iff] at h₁₂₃ h₃₂₁
simp_rw [← modEq_iff_eq_mod_zmultiples]
simpa only [modEq_comm] using toIxxMod_antisymm _ h₁₂₃ h₃₂₁
btw_total := fun x₁ x₂ x₃ => by
induction x₁ using QuotientAddGroup.induction_on
induction x₂ using QuotientAddGroup.induction_on
induction x₃ using QuotientAddGroup.induction_on
simp_rw [btw_coe_iff]
apply toIxxMod_total }
