Commit 2023-09-06 17:49 566dc2a5

View on Github →

chore: reduce imports of Data.Nat.Basic (#6974) Slightly delay the import of Mathlib.Algebra.Group.Basic, to reduce imports for tactics.

Estimated changes

Modified Mathlib/Algebra/ContinuedFractions/Translations.lean

Modified Mathlib/Algebra/GroupWithZero/Basic.lean

deleted theorem mul_left_inj'

deleted theorem mul_right_inj'

Modified Mathlib/Algebra/GroupWithZero/Defs.lean

added theorem mul_left_inj'

added theorem mul_right_inj'

Modified Mathlib/Data/Nat/Basic.lean

Modified Mathlib/Data/Nat/Bits.lean

Modified Mathlib/Data/Nat/PSub.lean

Modified Mathlib/Data/Set/Pointwise/Basic.lean