Commit 2024-11-13 10:39 6be28eb9

View on Github →

chore: camel cardinal_mk (#18808) Rename cardinal_mk in lemma names to cardinalMk to follow the naming convention.

Estimated changes

Modified Mathlib/Algebra/AlgebraicCard.lean

added theorem Algebraic.aleph0_le_cardinalMk_of_charZero

deleted theorem Algebraic.aleph0_le_cardinal_mk_of_charZero

added theorem Algebraic.cardinalMk_le_max

added theorem Algebraic.cardinalMk_le_mul

added theorem Algebraic.cardinalMk_lift_le_max

added theorem Algebraic.cardinalMk_lift_le_mul

added theorem Algebraic.cardinalMk_lift_of_infinite

added theorem Algebraic.cardinalMk_of_countable_of_charZero

added theorem Algebraic.cardinalMk_of_infinite

deleted theorem Algebraic.cardinal_mk_le_max

deleted theorem Algebraic.cardinal_mk_le_mul

deleted theorem Algebraic.cardinal_mk_lift_le_max

deleted theorem Algebraic.cardinal_mk_lift_le_mul

deleted theorem Algebraic.cardinal_mk_lift_of_infinite

deleted theorem Algebraic.cardinal_mk_of_countable_of_charZero

deleted theorem Algebraic.cardinal_mk_of_infinite

Modified Mathlib/Algebra/MvPolynomial/Cardinal.lean

added theorem MvPolynomial.cardinalMk_eq_lift

added theorem MvPolynomial.cardinalMk_eq_max

added theorem MvPolynomial.cardinalMk_eq_max_lift

added theorem MvPolynomial.cardinalMk_le_max

deleted theorem MvPolynomial.cardinal_mk_eq_lift

deleted theorem MvPolynomial.cardinal_mk_eq_max

deleted theorem MvPolynomial.cardinal_mk_eq_max_lift

deleted theorem MvPolynomial.cardinal_mk_le_max

Modified Mathlib/Algebra/Polynomial/Cardinal.lean

added theorem Polynomial.cardinalMk_eq_max

added theorem Polynomial.cardinalMk_le_max

deleted theorem Polynomial.cardinal_mk_eq_max

deleted theorem Polynomial.cardinal_mk_le_max

Modified Mathlib/Data/W/Cardinal.lean

added theorem WType.cardinalMk_eq_sum

added theorem WType.cardinalMk_eq_sum_lift

added theorem WType.cardinalMk_le_max_aleph0_of_finite'

added theorem WType.cardinalMk_le_max_aleph0_of_finite

added theorem WType.cardinalMk_le_of_le'

added theorem WType.cardinalMk_le_of_le

deleted theorem WType.cardinal_mk_eq_sum'

deleted theorem WType.cardinal_mk_eq_sum

deleted theorem WType.cardinal_mk_le_max_aleph0_of_finite'

deleted theorem WType.cardinal_mk_le_max_aleph0_of_finite

deleted theorem WType.cardinal_mk_le_of_le'

deleted theorem WType.cardinal_mk_le_of_le

Modified Mathlib/FieldTheory/Fixed.lean

added theorem cardinalMk_algHom

deleted theorem cardinal_mk_algHom

Modified Mathlib/FieldTheory/IsAlgClosed/Classification.lean

added theorem Algebra.IsAlgebraic.cardinalMk_le_max

added theorem Algebra.IsAlgebraic.cardinalMk_le_sigma_polynomial

deleted theorem Algebra.IsAlgebraic.cardinal_mk_le_max

deleted theorem Algebra.IsAlgebraic.cardinal_mk_le_sigma_polynomial

Modified Mathlib/LinearAlgebra/Dimension/DivisionRing.lean

Modified Mathlib/LinearAlgebra/Dimension/Finite.lean

added theorem LinearIndependent.cardinalMk_le_finrank

deleted theorem LinearIndependent.cardinal_mk_le_finrank

Modified Mathlib/LinearAlgebra/Dimension/FreeAndStrongRankCondition.lean

added theorem cardinalMk_eq_cardinalMk_field_pow_rank

deleted theorem cardinal_mk_eq_cardinal_mk_field_pow_rank

added theorem lift_cardinalMk_eq_lift_cardinalMk_field_pow_lift_rank

deleted theorem lift_cardinal_mk_eq_lift_cardinal_mk_field_pow_lift_rank

Modified Mathlib/LinearAlgebra/FreeModule/Finite/Matrix.lean

added theorem cardinalMk_algHom_le_rank

deleted theorem cardinal_mk_algHom_le_rank

Modified Mathlib/SetTheory/Cardinal/Basic.lean

Modified Mathlib/SetTheory/Cardinal/Subfield.lean

added theorem Subfield.cardinalMk_closure

added theorem Subfield.cardinalMk_closure_le_max

deleted theorem Subfield.cardinal_mk_closure

deleted theorem Subfield.cardinal_mk_closure_le_max

Modified scripts/no_lints_prime_decls.txt