Commit 2023-09-06 06:13 c161d180

View on Github →

chore: delay import of NeZero until after basic hierarchy (#6970)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Field/Defs.lean

Modified Mathlib/Algebra/Group/Defs.lean

Modified Mathlib/Algebra/GroupWithZero/Basic.lean

Modified Mathlib/Algebra/GroupWithZero/Defs.lean

deleted theorem pullback_nonzero

Modified Mathlib/Algebra/GroupWithZero/InjSurj.lean

Created Mathlib/Algebra/GroupWithZero/NeZero.lean

added theorem pullback_nonzero

Modified Mathlib/Algebra/NeZero.lean

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

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

Modified Mathlib/Algebra/Ring/Basic.lean

Modified Mathlib/GroupTheory/GroupAction/Opposite.lean

Modified Mathlib/GroupTheory/Submonoid/ZeroDivisors.lean

Modified Mathlib/Init/Algebra/Classes.lean

Modified Mathlib/Init/Algebra/Order.lean

Modified Mathlib/Logic/Nontrivial/Defs.lean

modified theorem exists_ne

Modified Mathlib/Tactic/Common.lean