Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-12-29 17:01 986c4d57

View on Github →

fix(*): mark some classes as Prop (#18015)

Estimated changes

Modified archive/100-theorems-list/30_ballot_problem.lean

Modified src/algebra/hom/freiman.lean

added theorem freiman_hom.freiman_hom_class_of_le

deleted def freiman_hom.freiman_hom_class_of_le

Modified src/algebraic_geometry/projective_spectrum/scheme.lean

Modified src/category_theory/monoidal/linear.lean

added theorem category_theory.monoidal_linear_of_faithful

deleted def category_theory.monoidal_linear_of_faithful

Modified src/category_theory/monoidal/preadditive.lean

added theorem category_theory.monoidal_preadditive_of_faithful

deleted def category_theory.monoidal_preadditive_of_faithful

Modified src/field_theory/subfield.lean

Modified src/group_theory/subgroup/basic.lean

Modified src/group_theory/submonoid/basic.lean

Modified src/group_theory/subsemigroup/basic.lean

Modified src/ring_theory/subring/basic.lean

Modified src/ring_theory/subsemiring/basic.lean