Commit 2023-07-27 15:45 930dd29d

View on Github →

feat: Linter that checks that Prop classes are Props (#6148)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Homology/Exact.lean

Modified Mathlib/Algebra/Jordan/Basic.lean

Modified Mathlib/Algebra/Lie/Basic.lean

added theorem LieModule.compLieHom

deleted def LieModule.compLieHom

modified def LieRingModule.compLieHom

Modified Mathlib/Algebra/Lie/OfAssociative.lean

added theorem LieModule.ofAssociativeModule

deleted def LieModule.ofAssociativeModule

Modified Mathlib/Algebra/Order/ZeroLEOne.lean

Modified Mathlib/Algebra/Ring/Defs.lean

Modified Mathlib/Algebra/Star/CHSH.lean

modified structure IsCHSHTuple

Modified Mathlib/Analysis/VonNeumannAlgebra/Basic.lean

Modified Mathlib/CategoryTheory/Closed/Functor.lean

added theorem CategoryTheory.cartesianClosedFunctorOfLeftAdjointPreservesBinaryProducts

deleted def CategoryTheory.cartesianClosedFunctorOfLeftAdjointPreservesBinaryProducts

Modified Mathlib/CategoryTheory/ConcreteCategory/BundledHom.lean

Modified Mathlib/CategoryTheory/ConcreteCategory/UnbundledHom.lean

Modified Mathlib/CategoryTheory/EpiMono.lean

Modified Mathlib/CategoryTheory/Functor/EpiMono.lean

added theorem CategoryTheory.Functor.splitEpiCategoryImpOfIsEquivalence

deleted def CategoryTheory.Functor.splitEpiCategoryImpOfIsEquivalence

Modified Mathlib/CategoryTheory/Limits/Shapes/Images.lean

Modified Mathlib/CategoryTheory/Monad/Monadicity.lean

Modified Mathlib/CategoryTheory/Noetherian.lean

Modified Mathlib/CategoryTheory/Triangulated/Triangulated.lean

Modified Mathlib/Combinatorics/Quiver/Symmetric.lean

Modified Mathlib/Control/Bifunctor.lean

Modified Mathlib/Control/Bitraversable/Basic.lean

Modified Mathlib/Control/Monad/Cont.lean

Modified Mathlib/Control/Traversable/Basic.lean

Modified Mathlib/Control/Traversable/Equiv.lean

Modified Mathlib/Data/Fin/Fin2.lean

Modified Mathlib/GroupTheory/GroupAction/SubMulAction.lean

added theorem SMulMemClass.ofIsScalarTower

deleted def SMulMemClass.ofIsScalarTower

Modified Mathlib/LinearAlgebra/TensorProduct.lean

Modified Mathlib/MeasureTheory/Group/Arithmetic.lean

Modified Mathlib/MeasureTheory/Measure/Doubling.lean

Modified Mathlib/ModelTheory/Basic.lean

added theorem FirstOrder.Language.HomClass.strongHomClassOfIsAlgebraic

deleted def FirstOrder.Language.HomClass.strongHomClassOfIsAlgebraic

Modified Mathlib/Order/RelClasses.lean

Modified Mathlib/Tactic.lean

Modified Mathlib/Tactic/Common.lean

Modified Mathlib/Tactic/Lift.lean

Created Mathlib/Tactic/Lint.lean

added def Std.Tactic.Lint.structureInType

Modified Mathlib/Topology/Order/Lattice.lean

Modified Mathlib/Topology/Order/Priestley.lean