Theorem one_z₂pow

Modification history

2023-11-01 16:07

Mathlib/Data/ZMod/IntUnitsPower.lean

chore(Data/ZMod/IntUnitsPower): rename lemmas (#8087) …

Deleted one_z₂pow View 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 one_z₂pow View on Github →