Commit 2025-06-06 01:24 343d2658

View on Github →

chore: trivial Nontrivialities (#25506) A bunch of Nontrivial instances are hiding inside DivisionRings and Fields and hold more generally.

Estimated changes

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

Modified Mathlib/Algebra/Order/CauSeq/Completion.lean

modified theorem CauSeq.Completion.mk_eq

added theorem CauSeq.Completion.ofRat_injective

Modified Mathlib/FieldTheory/PerfectClosure.lean

Modified Mathlib/Order/Atoms.lean

Modified Mathlib/RingTheory/Valuation/ValuationRing.lean

Modified Mathlib/Topology/Algebra/UniformField.lean