Commit 2024-09-16 14:35 a03152ba

View on Github →

chore: split Algebra.MonoidAlgebra.Basic (#16531) It's not the best justified split

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/FreeAlgebra.lean

Modified Mathlib/Algebra/MonoidAlgebra/Basic.lean

deleted theorem AddMonoidAlgebra.induction_on

deleted theorem AddMonoidAlgebra.intCast_def

deleted def AddMonoidAlgebra.liftNC

deleted def AddMonoidAlgebra.liftNCRingHom

deleted theorem AddMonoidAlgebra.liftNC_mul

deleted theorem AddMonoidAlgebra.liftNC_one

deleted theorem AddMonoidAlgebra.liftNC_single

deleted theorem AddMonoidAlgebra.liftNC_smul

deleted def AddMonoidAlgebra.mapDomainRingHom

deleted theorem AddMonoidAlgebra.mapDomain_mul

deleted theorem AddMonoidAlgebra.mapDomain_one

deleted theorem AddMonoidAlgebra.mapDomain_single

deleted theorem AddMonoidAlgebra.mapDomain_sum

deleted theorem AddMonoidAlgebra.mul_apply

deleted theorem AddMonoidAlgebra.mul_apply_antidiagonal

deleted theorem AddMonoidAlgebra.mul_def

deleted theorem AddMonoidAlgebra.mul_single_apply

deleted theorem AddMonoidAlgebra.mul_single_apply_aux

deleted theorem AddMonoidAlgebra.mul_single_apply_of_not_exists_add

deleted theorem AddMonoidAlgebra.mul_single_zero_apply

deleted theorem AddMonoidAlgebra.natCast_def

deleted def AddMonoidAlgebra.of'

deleted theorem AddMonoidAlgebra.of'_apply

deleted theorem AddMonoidAlgebra.of'_commute

deleted theorem AddMonoidAlgebra.of'_eq_of

deleted def AddMonoidAlgebra.of

deleted def AddMonoidAlgebra.ofMagma

deleted theorem AddMonoidAlgebra.of_apply

deleted theorem AddMonoidAlgebra.of_injective

deleted theorem AddMonoidAlgebra.one_def

deleted theorem AddMonoidAlgebra.opRingEquiv_single

deleted theorem AddMonoidAlgebra.opRingEquiv_symm_single

deleted theorem AddMonoidAlgebra.prod_single

deleted theorem AddMonoidAlgebra.ringHom_ext'

deleted theorem AddMonoidAlgebra.ringHom_ext

deleted def AddMonoidAlgebra.singleHom

deleted def AddMonoidAlgebra.singleZeroRingHom

deleted theorem AddMonoidAlgebra.single_add

deleted theorem AddMonoidAlgebra.single_apply

deleted theorem AddMonoidAlgebra.single_commute_single

deleted theorem AddMonoidAlgebra.single_eq_zero

deleted theorem AddMonoidAlgebra.single_mul_apply

deleted theorem AddMonoidAlgebra.single_mul_apply_aux

deleted theorem AddMonoidAlgebra.single_mul_apply_of_not_exists_add

deleted theorem AddMonoidAlgebra.single_mul_single

deleted theorem AddMonoidAlgebra.single_pow

deleted theorem AddMonoidAlgebra.single_zero

deleted theorem AddMonoidAlgebra.single_zero_mul_apply

deleted theorem AddMonoidAlgebra.sum_single

deleted theorem AddMonoidAlgebra.sum_single_index

deleted def AddMonoidAlgebra

deleted def MonoidAlgebra.comapDistribMulActionSelf

deleted theorem MonoidAlgebra.induction_on

deleted theorem MonoidAlgebra.intCast_def

deleted def MonoidAlgebra.liftNC

deleted def MonoidAlgebra.liftNCRingHom

deleted theorem MonoidAlgebra.liftNC_mul

deleted theorem MonoidAlgebra.liftNC_one

deleted theorem MonoidAlgebra.liftNC_single

deleted theorem MonoidAlgebra.liftNC_smul

deleted def MonoidAlgebra.mapDomainRingHom

deleted theorem MonoidAlgebra.mapDomain_mul

deleted theorem MonoidAlgebra.mapDomain_one

deleted theorem MonoidAlgebra.mapDomain_sum

deleted def MonoidAlgebra.mul'

deleted theorem MonoidAlgebra.mul_apply

deleted theorem MonoidAlgebra.mul_apply_antidiagonal

deleted theorem MonoidAlgebra.mul_apply_left

deleted theorem MonoidAlgebra.mul_apply_right

deleted theorem MonoidAlgebra.mul_def

deleted theorem MonoidAlgebra.mul_single_apply

deleted theorem MonoidAlgebra.mul_single_apply_aux

deleted theorem MonoidAlgebra.mul_single_apply_of_not_exists_mul

deleted theorem MonoidAlgebra.mul_single_one_apply

deleted theorem MonoidAlgebra.natCast_def

deleted def MonoidAlgebra.of

deleted def MonoidAlgebra.ofMagma

deleted theorem MonoidAlgebra.of_commute

deleted theorem MonoidAlgebra.of_injective

deleted theorem MonoidAlgebra.one_def

deleted theorem MonoidAlgebra.opRingEquiv_single

deleted theorem MonoidAlgebra.opRingEquiv_symm_single

deleted theorem MonoidAlgebra.prod_single

deleted theorem MonoidAlgebra.ringHom_ext'

deleted theorem MonoidAlgebra.ringHom_ext

deleted def MonoidAlgebra.singleHom

deleted def MonoidAlgebra.singleOneRingHom

deleted theorem MonoidAlgebra.single_add

deleted theorem MonoidAlgebra.single_apply

deleted theorem MonoidAlgebra.single_commute

deleted theorem MonoidAlgebra.single_commute_single

deleted theorem MonoidAlgebra.single_eq_zero

deleted theorem MonoidAlgebra.single_mul_apply

deleted theorem MonoidAlgebra.single_mul_apply_aux

deleted theorem MonoidAlgebra.single_mul_apply_of_not_exists_mul

deleted theorem MonoidAlgebra.single_mul_single

deleted theorem MonoidAlgebra.single_one_comm

deleted theorem MonoidAlgebra.single_one_mul_apply

deleted theorem MonoidAlgebra.single_pow

deleted theorem MonoidAlgebra.single_zero

deleted theorem MonoidAlgebra.smul_of

deleted def MonoidAlgebra.submoduleOfSMulMem

deleted theorem MonoidAlgebra.sum_single

deleted theorem MonoidAlgebra.sum_single_index

deleted def MonoidAlgebra

Created Mathlib/Algebra/MonoidAlgebra/Defs.lean

added theorem AddMonoidAlgebra.induction_on

added theorem AddMonoidAlgebra.intCast_def

added def AddMonoidAlgebra.liftNC

added def AddMonoidAlgebra.liftNCRingHom

added theorem AddMonoidAlgebra.liftNC_mul

added theorem AddMonoidAlgebra.liftNC_one

added theorem AddMonoidAlgebra.liftNC_single

added theorem AddMonoidAlgebra.liftNC_smul

added def AddMonoidAlgebra.mapDomainRingHom

added theorem AddMonoidAlgebra.mapDomain_mul

added theorem AddMonoidAlgebra.mapDomain_one

added theorem AddMonoidAlgebra.mapDomain_single

added theorem AddMonoidAlgebra.mapDomain_sum

added theorem AddMonoidAlgebra.mul_apply

added theorem AddMonoidAlgebra.mul_apply_antidiagonal

added theorem AddMonoidAlgebra.mul_def

added theorem AddMonoidAlgebra.mul_single_apply

added theorem AddMonoidAlgebra.mul_single_apply_aux

added theorem AddMonoidAlgebra.mul_single_apply_of_not_exists_add

added theorem AddMonoidAlgebra.mul_single_zero_apply

added theorem AddMonoidAlgebra.natCast_def

added def AddMonoidAlgebra.of'

added theorem AddMonoidAlgebra.of'_apply

added theorem AddMonoidAlgebra.of'_commute

added theorem AddMonoidAlgebra.of'_eq_of

added def AddMonoidAlgebra.of

added def AddMonoidAlgebra.ofMagma

added theorem AddMonoidAlgebra.of_apply

added theorem AddMonoidAlgebra.of_injective

added theorem AddMonoidAlgebra.one_def

added theorem AddMonoidAlgebra.opRingEquiv_single

added theorem AddMonoidAlgebra.opRingEquiv_symm_single

added theorem AddMonoidAlgebra.prod_single

added theorem AddMonoidAlgebra.ringHom_ext'

added theorem AddMonoidAlgebra.ringHom_ext

added def AddMonoidAlgebra.singleHom

added def AddMonoidAlgebra.singleZeroRingHom

added theorem AddMonoidAlgebra.single_add

added theorem AddMonoidAlgebra.single_apply

added theorem AddMonoidAlgebra.single_commute_single

added theorem AddMonoidAlgebra.single_eq_zero

added theorem AddMonoidAlgebra.single_mul_apply

added theorem AddMonoidAlgebra.single_mul_apply_aux

added theorem AddMonoidAlgebra.single_mul_apply_of_not_exists_add

added theorem AddMonoidAlgebra.single_mul_single

added theorem AddMonoidAlgebra.single_pow

added theorem AddMonoidAlgebra.single_zero

added theorem AddMonoidAlgebra.single_zero_mul_apply

added theorem AddMonoidAlgebra.sum_single

added theorem AddMonoidAlgebra.sum_single_index

added def AddMonoidAlgebra

added def MonoidAlgebra.comapDistribMulActionSelf

added theorem MonoidAlgebra.induction_on

added theorem MonoidAlgebra.intCast_def

added def MonoidAlgebra.liftNC

added def MonoidAlgebra.liftNCRingHom

added theorem MonoidAlgebra.liftNC_mul

added theorem MonoidAlgebra.liftNC_one

added theorem MonoidAlgebra.liftNC_single

added theorem MonoidAlgebra.liftNC_smul

added def MonoidAlgebra.mapDomainRingHom

added theorem MonoidAlgebra.mapDomain_mul

added theorem MonoidAlgebra.mapDomain_one

added theorem MonoidAlgebra.mapDomain_sum

added def MonoidAlgebra.mul'

added theorem MonoidAlgebra.mul_apply

added theorem MonoidAlgebra.mul_apply_antidiagonal

added theorem MonoidAlgebra.mul_apply_left

added theorem MonoidAlgebra.mul_apply_right

added theorem MonoidAlgebra.mul_def

added theorem MonoidAlgebra.mul_single_apply

added theorem MonoidAlgebra.mul_single_apply_aux

added theorem MonoidAlgebra.mul_single_apply_of_not_exists_mul

added theorem MonoidAlgebra.mul_single_one_apply

added theorem MonoidAlgebra.natCast_def

added def MonoidAlgebra.of

added def MonoidAlgebra.ofMagma

added theorem MonoidAlgebra.of_commute

added theorem MonoidAlgebra.of_injective

added theorem MonoidAlgebra.one_def

added theorem MonoidAlgebra.opRingEquiv_single

added theorem MonoidAlgebra.opRingEquiv_symm_single

added theorem MonoidAlgebra.prod_single

added theorem MonoidAlgebra.ringHom_ext'

added theorem MonoidAlgebra.ringHom_ext

added def MonoidAlgebra.singleHom

added def MonoidAlgebra.singleOneRingHom

added theorem MonoidAlgebra.single_add

added theorem MonoidAlgebra.single_apply

added theorem MonoidAlgebra.single_commute

added theorem MonoidAlgebra.single_commute_single

added theorem MonoidAlgebra.single_eq_zero

added theorem MonoidAlgebra.single_mul_apply

added theorem MonoidAlgebra.single_mul_apply_aux

added theorem MonoidAlgebra.single_mul_apply_of_not_exists_mul

added theorem MonoidAlgebra.single_mul_single

added theorem MonoidAlgebra.single_one_comm

added theorem MonoidAlgebra.single_one_mul_apply

added theorem MonoidAlgebra.single_pow

added theorem MonoidAlgebra.single_zero

added theorem MonoidAlgebra.smul_of

added def MonoidAlgebra.submoduleOfSMulMem

added theorem MonoidAlgebra.sum_single

added theorem MonoidAlgebra.sum_single_index

added def MonoidAlgebra

Modified Mathlib/Algebra/MonoidAlgebra/Division.lean

Modified Mathlib/Algebra/MonoidAlgebra/Grading.lean

Modified Mathlib/Algebra/MonoidAlgebra/Ideal.lean

Modified Mathlib/Algebra/MonoidAlgebra/NoZeroDivisors.lean

Modified Mathlib/Algebra/MonoidAlgebra/Support.lean

Modified Mathlib/Algebra/MvPolynomial/Basic.lean

Modified Mathlib/Algebra/Polynomial/AlgebraMap.lean

Modified Mathlib/Algebra/Polynomial/Basic.lean

Modified Mathlib/Algebra/Polynomial/DenomsClearable.lean

Modified Mathlib/Algebra/Polynomial/Eval.lean

Modified test/Polynomial.lean