Commit 2026-07-08 08:56 27c42f4d

View on Github →

chore(Algebra/SkewMonoidAlgebra): rename the conversion functions to coeff/ofCoeff (#41365)

Estimated changes

Modified Mathlib/Algebra/SkewMonoidAlgebra/Basic.lean

deleted def SkewMonoidAlgebra.coeff

added def SkewMonoidAlgebra.coeffAddEquiv

added def SkewMonoidAlgebra.coeffLinearEquiv

modified theorem SkewMonoidAlgebra.coeff_add

added theorem SkewMonoidAlgebra.coeff_eq_single_one_one_iff

added theorem SkewMonoidAlgebra.coeff_eq_zero

modified theorem SkewMonoidAlgebra.coeff_inj

modified theorem SkewMonoidAlgebra.coeff_injective

added theorem SkewMonoidAlgebra.coeff_mapDomain

added theorem SkewMonoidAlgebra.coeff_neg

added theorem SkewMonoidAlgebra.coeff_ofCoeff

deleted theorem SkewMonoidAlgebra.coeff_ofFinsupp

modified theorem SkewMonoidAlgebra.coeff_one

modified theorem SkewMonoidAlgebra.coeff_one_one

modified theorem SkewMonoidAlgebra.coeff_single

modified theorem SkewMonoidAlgebra.coeff_smul

added theorem SkewMonoidAlgebra.coeff_sub

added theorem SkewMonoidAlgebra.coeff_sum'

modified theorem SkewMonoidAlgebra.coeff_zero

modified theorem SkewMonoidAlgebra.eta

added theorem SkewMonoidAlgebra.ofCoeff_add

added theorem SkewMonoidAlgebra.ofCoeff_eq_one

added theorem SkewMonoidAlgebra.ofCoeff_eq_zero

added theorem SkewMonoidAlgebra.ofCoeff_inj

added theorem SkewMonoidAlgebra.ofCoeff_injective

added theorem SkewMonoidAlgebra.ofCoeff_neg

added theorem SkewMonoidAlgebra.ofCoeff_one

added theorem SkewMonoidAlgebra.ofCoeff_single

added theorem SkewMonoidAlgebra.ofCoeff_smul

added theorem SkewMonoidAlgebra.ofCoeff_sub

added theorem SkewMonoidAlgebra.ofCoeff_sum

added theorem SkewMonoidAlgebra.ofCoeff_zero

deleted theorem SkewMonoidAlgebra.ofFinsupp_add

deleted theorem SkewMonoidAlgebra.ofFinsupp_eq_one

deleted theorem SkewMonoidAlgebra.ofFinsupp_eq_zero

deleted theorem SkewMonoidAlgebra.ofFinsupp_inj

deleted theorem SkewMonoidAlgebra.ofFinsupp_injective

deleted theorem SkewMonoidAlgebra.ofFinsupp_neg

deleted theorem SkewMonoidAlgebra.ofFinsupp_one

deleted theorem SkewMonoidAlgebra.ofFinsupp_single

deleted theorem SkewMonoidAlgebra.ofFinsupp_smul

deleted theorem SkewMonoidAlgebra.ofFinsupp_sub

deleted theorem SkewMonoidAlgebra.ofFinsupp_sum

deleted theorem SkewMonoidAlgebra.ofFinsupp_zero

modified def SkewMonoidAlgebra.support

added theorem SkewMonoidAlgebra.support_coeff

added theorem SkewMonoidAlgebra.support_ofCoeff

deleted theorem SkewMonoidAlgebra.support_ofFinsupp

deleted theorem SkewMonoidAlgebra.support_toFinsupp

deleted def SkewMonoidAlgebra.toFinsuppAddEquiv

deleted def SkewMonoidAlgebra.toFinsuppLinearEquiv

deleted theorem SkewMonoidAlgebra.toFinsupp_add

modified theorem SkewMonoidAlgebra.toFinsupp_apply

deleted theorem SkewMonoidAlgebra.toFinsupp_eq_single_one_one_iff

deleted theorem SkewMonoidAlgebra.toFinsupp_eq_zero

deleted theorem SkewMonoidAlgebra.toFinsupp_inj

deleted theorem SkewMonoidAlgebra.toFinsupp_injective

deleted theorem SkewMonoidAlgebra.toFinsupp_mapDomain

deleted theorem SkewMonoidAlgebra.toFinsupp_neg

deleted theorem SkewMonoidAlgebra.toFinsupp_one

deleted theorem SkewMonoidAlgebra.toFinsupp_single

deleted theorem SkewMonoidAlgebra.toFinsupp_smul

deleted theorem SkewMonoidAlgebra.toFinsupp_sub

deleted theorem SkewMonoidAlgebra.toFinsupp_sum'

deleted theorem SkewMonoidAlgebra.toFinsupp_zero

Modified Mathlib/Algebra/SkewMonoidAlgebra/Lift.lean

deleted theorem SkewMonoidAlgebra.coeff_equivMapDomain

deleted theorem SkewMonoidAlgebra.toFinsupp_equivMapDomain

Modified Mathlib/Algebra/SkewMonoidAlgebra/Single.lean

deleted theorem SkewMonoidAlgebra.coeff_erase_apply

deleted theorem SkewMonoidAlgebra.coeff_update

modified def SkewMonoidAlgebra.update

modified theorem SkewMonoidAlgebra.update_self

Modified Mathlib/Algebra/SkewMonoidAlgebra/Support.lean

Modified Mathlib/Algebra/SkewPolynomial/Basic.lean