Theorem ZMod.natCast_smul_units

Modification history

2023-11-04 14:26
Mathlib/Data/ZMod/IntUnitsPower.lean
refactor(Data/ZMod/IntUnitsPower): generalize ZMod 2 to work for `Nat` and `Int` too (#7866) …
Added ZMod.natCast_smul_unitsView on Github →