Theorem ZMod.ker_intCastRingHom

Modification history

2024-05-05 17:09

Mathlib/Data/ZMod/Basic.lean

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

Modified ZMod.ker_intCastRingHom View on Github →

2024-04-17 11:15

Mathlib/Data/ZMod/Basic.lean

chore: Rename `nat_cast`/`int_cast`/`rat_cast` to `natCast`/`intCast`/`ratCast` (#11486) …

Added ZMod.ker_intCastRingHom View on Github →