Commit 2023-11-07 19:35 b7825966

View on Github →

chore: golf all coe_iSup_of_directed (#8232)

Estimated changes

Modified Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean

Modified Mathlib/Algebra/Algebra/Subalgebra/Basic.lean

modified theorem Subalgebra.coe_iSup_of_directed

modified def Subalgebra.equivOfEq

Modified Mathlib/Algebra/Star/NonUnitalSubalgebra.lean

Modified Mathlib/FieldTheory/Subfield.lean

Modified Mathlib/GroupTheory/Subgroup/Basic.lean

Modified Mathlib/GroupTheory/Submonoid/Membership.lean

Modified Mathlib/GroupTheory/Subsemigroup/Membership.lean

Modified Mathlib/LinearAlgebra/Span.lean

modified theorem Submodule.coe_iSup_of_directed

Modified Mathlib/RingTheory/NonUnitalSubring/Basic.lean

modified theorem NonUnitalSubring.coe_iSup_of_directed

Modified Mathlib/RingTheory/NonUnitalSubsemiring/Basic.lean

Modified Mathlib/RingTheory/Subring/Basic.lean

Modified Mathlib/RingTheory/Subsemiring/Basic.lean