Commit 2024-11-22 21:24 dd74f018

View on Github →

chore: split Algebra.Group.Nat (#19375)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Group/Int.lean

Created Mathlib/Algebra/Group/Nat/Basic.lean

Renamed Mathlib/Algebra/Group/Nat.lean to Mathlib/Algebra/Group/Nat/Even.lean

deleted theorem Nat.addUnits_eq_zero

deleted theorem Nat.ofAdd_mul

deleted theorem Nat.toAdd_pow

deleted theorem Nat.units_eq_one

Created Mathlib/Algebra/Group/Nat/TypeTags.lean

added theorem Nat.ofAdd_mul

added theorem Nat.toAdd_pow

Created Mathlib/Algebra/Group/Nat/Units.lean

added theorem Nat.addUnits_eq_zero

added theorem Nat.units_eq_one

Modified Mathlib/Algebra/Group/Submonoid/Operations.lean

Modified Mathlib/Algebra/GroupPower/IterateHom.lean

Modified Mathlib/Algebra/Order/Group/Nat.lean

Modified Mathlib/Algebra/Order/Ring/Basic.lean

Modified Mathlib/Algebra/Ring/Nat.lean

Modified Mathlib/Algebra/Ring/Parity.lean

Modified Mathlib/Data/List/SplitLengths.lean

Modified Mathlib/Data/Multiset/Basic.lean

Modified Mathlib/Data/Nat/Bits.lean

Modified Mathlib/Data/Nat/Bitwise.lean

Modified Mathlib/Data/Nat/Cast/Basic.lean

Modified Mathlib/Data/Nat/GCD/Basic.lean

Modified Mathlib/Data/Nat/PSub.lean

Modified Mathlib/Data/Nat/Prime/Defs.lean

Modified Mathlib/Data/Nat/Size.lean

Modified Mathlib/Data/Set/Enumerate.lean

Modified Mathlib/GroupTheory/SpecificGroups/Quaternion.lean

Modified Mathlib/Tactic/Sat/FromLRAT.lean

Modified MathlibTest/levenshtein.lean