Commit 2023-03-08 06:41 db9d23f6

View on Github →

feat: port Algebra.MonoidAlgebra.Basic (#2589)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/MonoidAlgebra/Basic.lean

added theorem AddMonoidAlgebra.algHom_ext'

added theorem AddMonoidAlgebra.algHom_ext

added theorem AddMonoidAlgebra.algHom_ext_iff

added theorem AddMonoidAlgebra.coe_algebraMap

added theorem AddMonoidAlgebra.induction_on

added theorem AddMonoidAlgebra.int_cast_def

added def AddMonoidAlgebra.lift

added def AddMonoidAlgebra.liftMagma

added def AddMonoidAlgebra.liftNC

added def AddMonoidAlgebra.liftNCAlgHom

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 theorem AddMonoidAlgebra.lift_apply'

added theorem AddMonoidAlgebra.lift_apply

added theorem AddMonoidAlgebra.lift_def

added theorem AddMonoidAlgebra.lift_of

added theorem AddMonoidAlgebra.lift_single

added theorem AddMonoidAlgebra.lift_symm_apply

added theorem AddMonoidAlgebra.lift_unique'

added theorem AddMonoidAlgebra.lift_unique

added def AddMonoidAlgebra.mapDomainAlgHom

added def AddMonoidAlgebra.mapDomainNonUnitalAlgHom

added def AddMonoidAlgebra.mapDomainRingHom

added theorem AddMonoidAlgebra.mapDomain_algebraMap

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_zero_apply

added theorem AddMonoidAlgebra.nat_cast_def

added theorem AddMonoidAlgebra.nonUnitalAlgHom_ext'

added theorem AddMonoidAlgebra.nonUnitalAlgHom_ext

added def AddMonoidAlgebra.of'

added theorem AddMonoidAlgebra.of'_apply

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.singleZeroAlgHom

added def AddMonoidAlgebra.singleZeroRingHom

added theorem AddMonoidAlgebra.single_add

added theorem AddMonoidAlgebra.single_apply

added theorem AddMonoidAlgebra.single_eq_zero

added theorem AddMonoidAlgebra.single_mul_apply

added theorem AddMonoidAlgebra.single_mul_apply_aux

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.toMultiplicativeAlgEquiv

added def AddMonoidAlgebra

added def MonoidAlgebra.GroupSmul.linearMap

added theorem MonoidAlgebra.GroupSmul.linearMap_apply

added theorem MonoidAlgebra.algHom_ext'

added theorem MonoidAlgebra.algHom_ext

added theorem MonoidAlgebra.coe_algebraMap

added def MonoidAlgebra.comapDistribMulActionSelf

added def MonoidAlgebra.equivariantOfLinearOfComm

added theorem MonoidAlgebra.equivariantOfLinearOfComm_apply

added theorem MonoidAlgebra.induction_on

added theorem MonoidAlgebra.int_cast_def

added def MonoidAlgebra.lift

added def MonoidAlgebra.liftMagma

added def MonoidAlgebra.liftNC

added def MonoidAlgebra.liftNCAlgHom

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 theorem MonoidAlgebra.lift_apply'

added theorem MonoidAlgebra.lift_apply

added theorem MonoidAlgebra.lift_def

added theorem MonoidAlgebra.lift_of

added theorem MonoidAlgebra.lift_single

added theorem MonoidAlgebra.lift_symm_apply

added theorem MonoidAlgebra.lift_unique'

added theorem MonoidAlgebra.lift_unique

added def MonoidAlgebra.mapDomainAlgHom

added def MonoidAlgebra.mapDomainNonUnitalAlgHom

added def MonoidAlgebra.mapDomainRingHom

added theorem MonoidAlgebra.mapDomain_algebraMap

added theorem MonoidAlgebra.mapDomain_mul

added theorem MonoidAlgebra.mapDomain_one

added theorem MonoidAlgebra.mapDomain_sum

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_one_apply

added theorem MonoidAlgebra.nat_cast_def

added theorem MonoidAlgebra.nonUnitalAlgHom_ext'

added theorem MonoidAlgebra.nonUnitalAlgHom_ext

added def MonoidAlgebra.of

added def MonoidAlgebra.ofMagma

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.singleOneAlgHom

added def MonoidAlgebra.singleOneRingHom

added theorem MonoidAlgebra.single_add

added theorem MonoidAlgebra.single_algebraMap_eq_algebraMap_mul_of

added theorem MonoidAlgebra.single_apply

added theorem MonoidAlgebra.single_eq_algebraMap_mul_of

added theorem MonoidAlgebra.single_eq_zero

added theorem MonoidAlgebra.single_mul_apply

added theorem MonoidAlgebra.single_mul_apply_aux

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.toAdditiveAlgEquiv

added def MonoidAlgebra