Theorem ZMod.smul_units_def

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.smul_units_defView on Github →