Commit 2025-05-12 14:24 e3053902

View on Github →

chore(Topology/Instances/AddCircle): golf and little lemmas (#23236)

Estimated changes

Modified Mathlib/Topology/Instances/AddCircle.lean

added theorem AddCircle.finite_torsion

added theorem AddCircle.intCast_div_mul_eq_zsmul

added theorem AddCircle.natCast_div_mul_eq_nsmul

added theorem AddCircle.nsmul_eq_zero_iff