Theorem ZMod.coe_intCast

Modification history

2024-07-24 14:17

Mathlib/Data/ZMod/Basic.lean

feat(ZMod): Simple lemmas (#15076) …

Modified ZMod.coe_intCast 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.coe_intCast View on Github →