Theorem zpow_coe_nat
Modification history
2024-03-20 12:03
Mathlib/Algebra/Group/Defs.lean
chore: Rename `zpow_coe_nat` to `zpow_natCast` (#11528) …
Deleted zpow_coe_natView on Github →2024-02-27 17:09
Mathlib/Algebra/Group/Defs.lean
fix: correct statement of `zpow_ofNat` and `ofNat_zsmul` (#10969) …
Modified zpow_coe_natView on Github →2024-01-05 11:32
Mathlib/Algebra/Group/Defs.lean
chore: Move `Commute` results earlier (#9440) …
Modified zpow_coe_natView on Github →2023-02-17 17:10
Mathlib/Data/Int/Basic.lean
feat: to_additive raises linter errors; nested to_additive (#1819) …
Modified zpow_coe_natView on Github →2022-12-04 13:00
Mathlib/Algebra/Ring/Basic.lean
feat: port algebra.ring.basic (#830) …
Modified zpow_coe_natView on Github →