Theorem z₂pow_natCast

Modification history

2023-11-01 16:07
Mathlib/Data/ZMod/IntUnitsPower.lean
chore(Data/ZMod/IntUnitsPower): rename lemmas (#8087) …
Deleted z₂pow_natCastView on Github →
2023-10-23 14:19
Mathlib/Data/ZMod/IntUnitsPower.lean
feat(Data/ZMod/IntUnitsPower): The power operator by `ZMod 2` on `ℤˣ` (#7661) …
Added z₂pow_natCastView on Github →