Commit 2023-09-05 09:13 560425d2

View on Github →

feat: split Logic.Nontrivial (#6959) This continues reducing the import requirements for the basic algebraic hierarchy. In combination with #6954 #6955 #6956 #6957, this reduces the imports for Mathlib.Algebra.Field.Defs from

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/EuclideanDomain/Defs.lean

Modified Mathlib/Algebra/Group/TypeTags.lean

Modified Mathlib/Algebra/Group/ULift.lean

Modified Mathlib/Algebra/Group/Units.lean

Modified Mathlib/Algebra/GroupWithZero/Defs.lean

Modified Mathlib/Algebra/GroupWithZero/Units/Basic.lean

Modified Mathlib/Algebra/Opposites.lean

Modified Mathlib/Data/Int/Basic.lean

Modified Mathlib/Data/TwoPointing.lean

Created Mathlib/Logic/Nontrivial/Basic.lean

added theorem Pi.nontrivial_at

added theorem Subsingleton.eq_one

added theorem Subtype.nontrivial_iff_exists_ne

added theorem exists_pair_lt

added theorem nontrivial_iff_lt

added theorem nontrivial_of_lt

Renamed Mathlib/Logic/Nontrivial.lean to Mathlib/Logic/Nontrivial/Defs.lean

deleted theorem Pi.nontrivial_at

deleted theorem Subsingleton.eq_one

deleted theorem Subtype.nontrivial_iff_exists_ne

deleted theorem exists_pair_lt

deleted theorem nontrivial_iff_lt

deleted theorem nontrivial_of_lt

Modified Mathlib/Order/Synonym.lean

Modified Mathlib/Order/WithBot.lean

Modified Mathlib/Tactic/Nontriviality/Core.lean