Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-11-29 08:55 fc6ece0a

View on Github →

chore(algebra/order/to_interval_mod): add equiv versions extracted from add_circle (#17739)

Estimated changes

Modified src/algebra/order/to_interval_mod.lean

added def quotient_add_group.equiv_Ico_mod

added theorem quotient_add_group.equiv_Ico_mod_coe

added def quotient_add_group.equiv_Ioc_mod

added theorem quotient_add_group.equiv_Ioc_mod_coe

Modified src/topology/instances/add_circle.lean

modified theorem add_circle.coe_image_Icc_eq

added theorem add_circle.coe_image_Ico_eq