Commit 2023-04-24 22:04 6223f212

View on Github →

chore: tidy various files (#3629)

Estimated changes

Modified Mathlib/Algebra/RingQuot.lean

Modified Mathlib/AlgebraicTopology/DoldKan/Degeneracies.lean

Modified Mathlib/CategoryTheory/Yoneda.lean

modified def CategoryTheory.coyoneda

modified def CategoryTheory.yoneda

modified def CategoryTheory.yonedaLemma

Modified Mathlib/LinearAlgebra/Dimension.lean

Modified Mathlib/LinearAlgebra/Multilinear/Basic.lean

deleted theorem MultilinearMap.coe_curr_sum_equiv_symm

added theorem MultilinearMap.coe_currySumEquiv_symm

Modified Mathlib/LinearAlgebra/SesquilinearForm.lean

deleted theorem LinearMap.IsOrthoᵢ.nondegenerateOfNotIsOrthoBasisSelf

added theorem LinearMap.IsOrthoᵢ.nondegenerate_of_not_isOrtho_basis_self

deleted theorem LinearMap.IsOrthoᵢ.separatingLeftOfNotIsOrthoBasisSelf

added theorem LinearMap.IsOrthoᵢ.separatingLeft_of_not_isOrtho_basis_self

deleted theorem LinearMap.IsOrthoᵢ.separatingRightIffNotIsOrthoBasisSelf

added theorem LinearMap.IsOrthoᵢ.separatingRight_iff_not_isOrtho_basis_self

added theorem LinearMap.IsRefl.domRestrict

deleted theorem LinearMap.IsRefl.domRestrictRefl

deleted theorem LinearMap.IsRefl.nondegenerateOfSeparatingLeft

deleted theorem LinearMap.IsRefl.nondegenerateOfSeparatingRight

added theorem LinearMap.IsRefl.nondegenerate_of_separatingLeft

added theorem LinearMap.IsRefl.nondegenerate_of_separatingRight

added theorem LinearMap.IsSymm.domRestrict

deleted theorem LinearMap.IsSymm.domRestrictSymm

deleted theorem LinearMap.isAdjointPairId

deleted theorem LinearMap.isAdjointPairZero

added theorem LinearMap.isAdjointPair_id

added theorem LinearMap.isAdjointPair_zero

deleted theorem LinearMap.isOrthoZeroLeft

deleted theorem LinearMap.isOrthoZeroRight

added theorem LinearMap.isOrtho_zero_left

added theorem LinearMap.isOrtho_zero_right

modified def LinearMap.isPairSelfAdjointSubmodule

Modified Mathlib/Topology/MetricSpace/HausdorffDistance.lean