Commit 2024-05-05 17:09 927ceb40

View on Github →

chore: reduce imports in ZMod.Basic (#12478)

While at it, document the lemmas that were moved, and two similar lemmas in ZMod.Basic.

Estimated changes

Modified Mathlib/Data/ZMod/Basic.lean

deleted theorem ZMod.ker_intCastRingHom

deleted theorem ZMod.ringHom_eq_of_ker_eq

Modified Mathlib/Data/ZMod/Module.lean

Modified Mathlib/Data/ZMod/Quotient.lean

Modified Mathlib/Data/ZMod/Units.lean

Modified Mathlib/NumberTheory/Padics/RingHoms.lean

Modified Mathlib/RingTheory/ZMod.lean

added theorem ZMod.ker_intCastRingHom

added theorem ZMod.ringHom_eq_of_ker_eq

Modified Mathlib/Topology/Instances/Real.lean