Commit 2023-09-01 20:13 cda5caa7

View on Github →

chore: tidy various files (#6838)

Estimated changes

Modified Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean

Modified Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean

Modified Mathlib/Algebra/RingQuot.lean

Modified Mathlib/Data/Set/Finite.lean

Modified Mathlib/Data/Set/Image.lean

Modified Mathlib/LinearAlgebra/Basic.lean

modified def LinearMap.applyₗ'

modified def LinearMap.compRight

modified def LinearMap.domRestrict'

modified def LinearMap.evalAddMonoidHom

modified def LinearMap.funLeft

modified def LinearMap.iterateKer

modified def LinearMap.iterateRange

modified def LinearMap.smulRight

modified def LinearMap.smulRightₗ

modified def LinearMap.toAddMonoidHom'

modified def Submodule.comapSubtypeEquivOfLe

modified def Submodule.compatibleMaps

added theorem Submodule.map_toAddSubmonoid'

deleted theorem Submodule.map_to_add_submonoid'

modified def Submodule.orderIsoMapComap

Modified Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean

Modified Mathlib/LinearAlgebra/TensorAlgebra/Basic.lean

Modified Mathlib/LinearAlgebra/Trace.lean

Modified Mathlib/Topology/Category/CompHaus/Limits.lean

Modified Mathlib/Topology/Category/Stonean/Basic.lean

Modified Mathlib/Topology/Category/Stonean/Limits.lean

Modified Mathlib/Topology/ContinuousFunction/Algebra.lean

Modified Mathlib/Topology/ExtremallyDisconnected.lean

Modified Mathlib/Topology/LocalHomeomorph.lean

Modified Mathlib/Topology/Order/LowerUpperTopology.lean

deleted theorem LowerDual_iff_Upper

deleted theorem UpperDual_iff_Lower

added theorem lower_dual_iff_upper

added theorem upper_dual_iff_lower