MapDomain

📁 Source: Mathlib/Algebra/MonoidAlgebra/MapDomain.lean

Statistics

Metric	Count
Definitions `commRingEquiv`, `mapDomain`, `mapDomainAddEquiv`, `mapDomainNonUnitalRingHom`, `mapDomainRingEquiv`, `mapDomainRingHom`, `mapRangeAddEquiv`, `mapRangeRingEquiv`, `mapRangeRingHom`, `toMultiplicative`, `commRingEquiv`, `mapDomain`, `mapDomainAddEquiv`, `mapDomainNonUnitalRingHom`, `mapDomainRingEquiv`, `mapDomainRingHom`, `mapRangeAddEquiv`, `mapRangeRingEquiv`, `mapRangeRingHom`	19
Theorems `coe_mapRangeRingHom`, `commRingEquiv_single_single`, `mapDomainAddEquiv_apply`, `mapDomainAddEquiv_single`, `mapDomainAddEquiv_trans`, `mapDomainNonUnitalRingHom_apply`, `mapDomainNonUnitalRingHom_comp`, `mapDomainNonUnitalRingHom_id`, `mapDomainRingEquiv_apply`, `mapDomainRingEquiv_single`, `mapDomainRingEquiv_trans`, `mapDomainRingHom_apply`, `mapDomainRingHom_comp`, `mapDomainRingHom_id`, `mapDomain_add`, `mapDomain_injective`, `mapDomain_mul`, `mapDomain_one`, `mapDomain_single`, `mapDomain_sum`, `mapDomain_zero`, `mapRangeAddEquiv_apply`, `mapRangeAddEquiv_single`, `mapRangeAddEquiv_trans`, `mapRangeRingEquiv_apply`, `mapRangeRingEquiv_single`, `mapRangeRingEquiv_trans`, `mapRangeRingHom_apply`, `mapRangeRingHom_comp`, `mapRangeRingHom_comp_mapDomainRingHom`, `mapRangeRingHom_id`, `mapRangeRingHom_single`, `symm_commRingEquiv`, `symm_mapDomainAddEquiv`, `symm_mapDomainRingEquiv`, `symm_mapRangeAddEquiv`, `symm_mapRangeRingEquiv`, `toRingHom_mapDomainRingEquiv`, `toRingHom_mapRangeRingEquiv`, `coe_mapRangeRingHom`, `commRingEquiv_single_single`, `mapDomainAddEquiv_apply`, `mapDomainAddEquiv_single`, `mapDomainAddEquiv_trans`, `mapDomainNonUnitalRingHom_apply`, `mapDomainNonUnitalRingHom_comp`, `mapDomainNonUnitalRingHom_id`, `mapDomainRingEquiv_apply`, `mapDomainRingEquiv_single`, `mapDomainRingEquiv_trans`, `mapDomainRingHom_apply`, `mapDomainRingHom_comp`, `mapDomainRingHom_id`, `mapDomain_add`, `mapDomain_injective`, `mapDomain_mul`, `mapDomain_one`, `mapDomain_single`, `mapDomain_sum`, `mapDomain_zero`, `mapRangeAddEquiv_apply`, `mapRangeAddEquiv_single`, `mapRangeAddEquiv_trans`, `mapRangeRingEquiv_apply`, `mapRangeRingEquiv_single`, `mapRangeRingEquiv_trans`, `mapRangeRingHom_apply`, `mapRangeRingHom_comp`, `mapRangeRingHom_comp_mapDomainRingHom`, `mapRangeRingHom_id`, `mapRangeRingHom_single`, `ringHom_ext_iff`, `symm_commRingEquiv`, `symm_mapDomainAddEquiv`, `symm_mapDomainRingEquiv`, `symm_mapRangeAddEquiv`, `symm_mapRangeRingEquiv`, `toRingHom_mapDomainRingEquiv`, `toRingHom_mapRangeRingEquiv`	79
Total	98

AddMonoidAlgebra

Definitions

Name	Category	Theorems
`commRingEquiv` 📖	CompOp	2 math math: `commRingEquiv_single_single`, `symm_commRingEquiv`
`mapDomain` 📖	CompOp	13 math math: `mapDomain_one`, `mapDomainNonUnitalRingHom_apply`, `mapDomainBialgHom_apply`, `Polynomial.toLaurent_apply`, `mapDomainAlgHom_apply`, `mapDomain_algebraMap`, `mapDomain_mul`, `mapDomain_zero`, `mapDomain_add`, `mapDomain_single`, `mapDomain_sum`, `mapDomain_injective`, `mapDomainRingHom_apply`
`mapDomainAddEquiv` 📖	CompOp	4 math math: `mapDomainAddEquiv_single`, `mapDomainAddEquiv_apply`, `mapDomainAddEquiv_trans`, `symm_mapDomainAddEquiv`
`mapDomainNonUnitalRingHom` 📖	CompOp	4 math math: `mapDomainNonUnitalRingHom_id`, `mapDomainNonUnitalAlgHom_apply`, `mapDomainNonUnitalRingHom_apply`, `mapDomainNonUnitalRingHom_comp`
`mapDomainRingEquiv` 📖	CompOp	5 math math: `mapDomainRingEquiv_apply`, `toRingHom_mapDomainRingEquiv`, `mapDomainRingEquiv_trans`, `mapDomainRingEquiv_single`, `symm_mapDomainRingEquiv`
`mapDomainRingHom` 📖	CompOp	6 math math: `toRingHom_mapDomainRingEquiv`, `mapDomainRingHom_comp_algebraMap`, `mapDomainRingHom_comp`, `mapDomainRingHom_id`, `mapRangeRingHom_comp_mapDomainRingHom`, `mapDomainRingHom_apply`
`mapRangeAddEquiv` 📖	CompOp	4 math math: `mapRangeAddEquiv_apply`, `mapRangeAddEquiv_trans`, `mapRangeAddEquiv_single`, `symm_mapRangeAddEquiv`
`mapRangeRingEquiv` 📖	CompOp	5 math math: `toRingHom_mapRangeRingEquiv`, `mapRangeRingEquiv_trans`, `mapRangeRingEquiv_apply`, `symm_mapRangeRingEquiv`, `mapRangeRingEquiv_single`
`mapRangeRingHom` 📖	CompOp	11 math math: `toRingHom_mapRangeRingEquiv`, `lift_mapRangeRingHom_algebraMap`, `mapRangeRingHom_comp_algebraMap`, `algebraMap_def`, `mapRangeRingHom_single`, `mapRangeRingHom_apply`, `mapRangeRingHom_comp`, `coe_mapRangeRingHom`, `toRingHom_mapRangeAlgHom`, `mapRangeRingHom_id`, `mapRangeRingHom_comp_mapDomainRingHom`
`toMultiplicative` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_mapRangeRingHom` 📖	mathematical	—	`DFunLike.coe` `RingHom` `AddMonoidAlgebra` `nonAssocSemiring` `AddMonoid.toAddZeroClass` `RingHom.instFunLike` `mapRangeRingHom` `Finsupp.mapRange` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `NonAssocSemiring.toMulZeroOneClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`	—	—
`commRingEquiv_single_single` 📖	mathematical	—	`DFunLike.coe` `RingEquiv` `AddMonoidAlgebra` `semiring` `instMul` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `nonUnitalNonAssocSemiring` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `commRingEquiv` `single`	—	`Finsupp.uncurry_single` `Finsupp.mapDomain_single` `Finsupp.curry_single`
`mapDomainAddEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instFunLike` `AddEquiv` `AddMonoidAlgebra` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `nonUnitalNonAssocSemiring` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `mapDomainAddEquiv` `Equiv` `Equiv.instEquivLike` `Equiv.symm`	—	`Finsupp.mapDomain_equiv_apply`
`mapDomainAddEquiv_single` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `AddMonoidAlgebra` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `nonUnitalNonAssocSemiring` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `mapDomainAddEquiv` `single` `Equiv` `Equiv.instEquivLike`	—	`Finsupp.mapDomain_single`
`mapDomainAddEquiv_trans` 📖	mathematical	—	`mapDomainAddEquiv` `Equiv.trans` `AddEquiv.trans` `AddMonoidAlgebra` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `nonUnitalNonAssocSemiring`	—	`AddEquiv.ext` `ext` `mapDomainAddEquiv_apply`
`mapDomainNonUnitalRingHom_apply` 📖	mathematical	—	`DFunLike.coe` `NonUnitalRingHom` `AddMonoidAlgebra` `nonUnitalNonAssocSemiring` `NonUnitalRingHom.instFunLike` `mapDomainNonUnitalRingHom` `mapDomain` `AddHom` `AddHom.funLike`	—	—
`mapDomainNonUnitalRingHom_comp` 📖	mathematical	—	`mapDomainNonUnitalRingHom` `AddHom.comp` `NonUnitalRingHom.comp` `AddMonoidAlgebra` `nonUnitalNonAssocSemiring`	—	`NonUnitalRingHom.ext` `ext` `Finsupp.mapDomain_comp`
`mapDomainNonUnitalRingHom_id` 📖	mathematical	—	`mapDomainNonUnitalRingHom` `AddHom.id` `NonUnitalRingHom.id` `AddMonoidAlgebra` `nonUnitalNonAssocSemiring`	—	`NonUnitalRingHom.ext` `ext` `Finsupp.mapDomain_id`
`mapDomainRingEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instFunLike` `RingEquiv` `AddMonoidAlgebra` `instMul` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `nonUnitalNonAssocSemiring` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `mapDomainRingEquiv` `AddEquiv` `AddEquiv.instEquivLike` `AddEquiv.symm`	—	`mapDomainAddEquiv_apply`
`mapDomainRingEquiv_single` 📖	mathematical	—	`DFunLike.coe` `RingEquiv` `AddMonoidAlgebra` `instMul` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `nonUnitalNonAssocSemiring` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `mapDomainRingEquiv` `single` `AddEquiv` `AddEquiv.instEquivLike`	—	`Finsupp.mapDomain_single`
`mapDomainRingEquiv_trans` 📖	mathematical	—	`mapDomainRingEquiv` `AddEquiv.trans` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `RingEquiv.trans` `AddMonoidAlgebra` `instMul` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `nonUnitalNonAssocSemiring`	—	`RingEquiv.ext` `ext` `mapDomainRingEquiv_apply`
`mapDomainRingHom_apply` 📖	mathematical	—	`DFunLike.coe` `RingHom` `AddMonoidAlgebra` `nonAssocSemiring` `AddMonoid.toAddZeroClass` `RingHom.instFunLike` `mapDomainRingHom` `mapDomain` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoidHom.instFunLike`	—	—
`mapDomainRingHom_comp` 📖	mathematical	—	`mapDomainRingHom` `AddMonoidHom.comp` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `RingHom.comp` `AddMonoidAlgebra` `nonAssocSemiring`	—	`ringHom_ext` `ext` `Finsupp.mapDomain_single` `map_zero` `AddMonoidHomClass.toZeroHomClass` `AddMonoidHom.instAddMonoidHomClass`
`mapDomainRingHom_id` 📖	mathematical	—	`mapDomainRingHom` `AddMonoidHom.id` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `RingHom.id` `AddMonoidAlgebra` `nonAssocSemiring`	—	`ringHom_ext` `ext` `Finsupp.mapDomain_single`
`mapDomain_add` 📖	mathematical	—	`mapDomain` `AddMonoidAlgebra` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `addAddCommMonoid`	—	`Finsupp.mapDomain_add`
`mapDomain_injective` 📖	mathematical	—	`AddMonoidAlgebra` `mapDomain`	—	`Finsupp.mapDomain_injective`
`mapDomain_mul` 📖	mathematical	—	`mapDomain` `DFunLike.coe` `AddMonoidAlgebra` `instMul`	—	`mul_def` `mapDomain_sum` `Finsupp.mapDomain_single` `map_add` `Finsupp.sum_mapDomain_index` `MulZeroClass.mul_zero` `Finsupp.single_zero` `mul_add` `Distrib.leftDistribClass` `Finsupp.single_add` `MulZeroClass.zero_mul` `Finsupp.sum_fun_zero` `add_mul` `Distrib.rightDistribClass` `Finsupp.sum_add`
`mapDomain_one` 📖	mathematical	—	`mapDomain` `DFunLike.coe` `AddMonoidAlgebra` `zero`	—	`Finsupp.mapDomain_single` `map_zero`
`mapDomain_single` 📖	mathematical	—	`mapDomain` `single`	—	`ext` `Finsupp.mapDomain_single`
`mapDomain_sum` 📖	mathematical	—	`mapDomain` `Finsupp.sum` `AddMonoidAlgebra` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `addAddCommMonoid`	—	`Finsupp.mapDomain_sum`
`mapDomain_zero` 📖	mathematical	—	`mapDomain` `AddMonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `addAddCommMonoid`	—	`Finsupp.mapDomain_zero`
`mapRangeAddEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instFunLike` `AddEquiv` `AddMonoidAlgebra` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `nonUnitalNonAssocSemiring` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `mapRangeAddEquiv`	—	—
`mapRangeAddEquiv_single` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `AddMonoidAlgebra` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `nonUnitalNonAssocSemiring` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `mapRangeAddEquiv` `single` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`Finsupp.mapRange_single`
`mapRangeAddEquiv_trans` 📖	mathematical	—	`mapRangeAddEquiv` `AddEquiv.trans` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddMonoidAlgebra` `nonUnitalNonAssocSemiring`	—	`AddEquiv.ext` `ext` `mapRangeAddEquiv_apply`
`mapRangeRingEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instFunLike` `RingEquiv` `AddMonoidAlgebra` `instMul` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `nonUnitalNonAssocSemiring` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `mapRangeRingEquiv` `Distrib.toMul`	—	`mapRangeRingHom_apply`
`mapRangeRingEquiv_single` 📖	mathematical	—	`DFunLike.coe` `RingEquiv` `AddMonoidAlgebra` `instMul` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `nonUnitalNonAssocSemiring` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `mapRangeRingEquiv` `single` `Distrib.toMul` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`mapRangeRingHom_single`
`mapRangeRingEquiv_trans` 📖	mathematical	—	`mapRangeRingEquiv` `RingEquiv.trans` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toAdd` `AddMonoidAlgebra` `instMul` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `nonUnitalNonAssocSemiring`	—	`RingEquiv.ext` `ext` `mapRangeRingEquiv_apply`
`mapRangeRingHom_apply` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instFunLike` `RingHom` `AddMonoidAlgebra` `nonAssocSemiring` `AddMonoid.toAddZeroClass` `RingHom.instFunLike` `mapRangeRingHom`	—	—
`mapRangeRingHom_comp` 📖	mathematical	—	`mapRangeRingHom` `RingHom.comp` `Semiring.toNonAssocSemiring` `AddMonoidAlgebra` `nonAssocSemiring` `AddMonoid.toAddZeroClass`	—	`ringHom_ext` `ext` `mapRangeRingHom_single` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`
`mapRangeRingHom_comp_mapDomainRingHom` 📖	mathematical	—	`RingHom.comp` `AddMonoidAlgebra` `nonAssocSemiring` `AddMonoid.toAddZeroClass` `mapRangeRingHom` `mapDomainRingHom`	—	`ringHom_ext` `ext` `Finsupp.mapDomain_single` `map_zero` `AddMonoidHomClass.toZeroHomClass` `AddMonoidHom.instAddMonoidHomClass` `mapRangeRingHom_single` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`
`mapRangeRingHom_id` 📖	mathematical	—	`mapRangeRingHom` `RingHom.id` `Semiring.toNonAssocSemiring` `AddMonoidAlgebra` `nonAssocSemiring` `AddMonoid.toAddZeroClass`	—	`ringHom_ext` `ext` `mapRangeRingHom_single`
`mapRangeRingHom_single` 📖	mathematical	—	`DFunLike.coe` `RingHom` `AddMonoidAlgebra` `nonAssocSemiring` `AddMonoid.toAddZeroClass` `RingHom.instFunLike` `mapRangeRingHom` `single` `Semiring.toNonAssocSemiring`	—	`ext` `mapRangeRingHom_apply` `single_apply` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`
`symm_commRingEquiv` 📖	mathematical	—	`RingEquiv.symm` `AddMonoidAlgebra` `semiring` `instMul` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `nonUnitalNonAssocSemiring` `commRingEquiv`	—	—
`symm_mapDomainAddEquiv` 📖	mathematical	—	`AddEquiv.symm` `AddMonoidAlgebra` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `nonUnitalNonAssocSemiring` `mapDomainAddEquiv` `Equiv.symm`	—	—
`symm_mapDomainRingEquiv` 📖	mathematical	—	`RingEquiv.symm` `AddMonoidAlgebra` `instMul` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `nonUnitalNonAssocSemiring` `mapDomainRingEquiv` `AddEquiv.symm`	—	—
`symm_mapRangeAddEquiv` 📖	mathematical	—	`AddEquiv.symm` `AddMonoidAlgebra` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `nonUnitalNonAssocSemiring` `mapRangeAddEquiv` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	—
`symm_mapRangeRingEquiv` 📖	mathematical	—	`RingEquiv.symm` `AddMonoidAlgebra` `instMul` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `nonUnitalNonAssocSemiring` `mapRangeRingEquiv` `Distrib.toMul` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	—
`toRingHom_mapDomainRingEquiv` 📖	mathematical	—	`RingEquiv.toRingHom` `AddMonoidAlgebra` `nonAssocSemiring` `AddMonoid.toAddZeroClass` `mapDomainRingEquiv` `mapDomainRingHom` `AddMonoidHomClass.toAddMonoidHom` `AddEquiv` `AddZero.toAdd` `AddZeroClass.toAddZero` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `AddEquivClass.instAddMonoidHomClass` `AddEquiv.instAddEquivClass`	—	—
`toRingHom_mapRangeRingEquiv` 📖	mathematical	—	`RingEquiv.toRingHom` `AddMonoidAlgebra` `nonAssocSemiring` `AddMonoid.toAddZeroClass` `mapRangeRingEquiv` `mapRangeRingHom` `RingHomClass.toRingHom` `RingEquiv` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass`	—	—

MonoidAlgebra

Definitions

Name	Category	Theorems
`commRingEquiv` 📖	CompOp	2 math math: `symm_commRingEquiv`, `commRingEquiv_single_single`
`mapDomain` 📖	CompOp	12 math math: `mapDomain_algebraMap`, `mapDomain_injective`, `mapDomainBialgHom_apply`, `mapDomainNonUnitalRingHom_apply`, `mapDomain_single`, `mapDomain_zero`, `mapDomain_one`, `mapDomainRingHom_apply`, `mapDomain_sum`, `mapDomain_mul`, `mapDomainAlgHom_apply`, `mapDomain_add`
`mapDomainAddEquiv` 📖	CompOp	4 math math: `symm_mapDomainAddEquiv`, `mapDomainAddEquiv_single`, `mapDomainAddEquiv_trans`, `mapDomainAddEquiv_apply`
`mapDomainNonUnitalRingHom` 📖	CompOp	4 math math: `mapDomainNonUnitalRingHom_id`, `mapDomainNonUnitalRingHom_apply`, `mapDomainNonUnitalAlgHom_apply`, `mapDomainNonUnitalRingHom_comp`
`mapDomainRingEquiv` 📖	CompOp	5 math math: `mapDomainRingEquiv_single`, `mapDomainRingEquiv_trans`, `toRingHom_mapDomainRingEquiv`, `mapDomainRingEquiv_apply`, `symm_mapDomainRingEquiv`
`mapDomainRingHom` 📖	CompOp	7 math math: `mapDomainRingHom_id`, `mapRangeRingHom_comp_mapDomainRingHom`, `toRingHom_mapDomainRingEquiv`, `CommRingCat.monoidAlgebra_map`, `mapDomainRingHom_comp`, `mapDomainRingHom_apply`, `mapDomainRingHom_comp_algebraMap`
`mapRangeAddEquiv` 📖	CompOp	4 math math: `mapRangeAddEquiv_apply`, `mapRangeAddEquiv_trans`, `symm_mapRangeAddEquiv`, `mapRangeAddEquiv_single`
`mapRangeRingEquiv` 📖	CompOp	5 math math: `mapRangeRingEquiv_single`, `symm_mapRangeRingEquiv`, `mapRangeRingEquiv_apply`, `mapRangeRingEquiv_trans`, `toRingHom_mapRangeRingEquiv`
`mapRangeRingHom` 📖	CompOp	11 math math: `mapRangeRingHom_single`, `toRingHom_mapRangeAlgHom`, `coe_mapRangeRingHom`, `mapRangeRingHom_comp_mapDomainRingHom`, `mapRangeRingHom_comp_algebraMap`, `algebraMap_def`, `lift_mapRangeRingHom_algebraMap`, `toRingHom_mapRangeRingEquiv`, `mapRangeRingHom_id`, `mapRangeRingHom_comp`, `mapRangeRingHom_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_mapRangeRingHom` 📖	mathematical	—	`DFunLike.coe` `RingHom` `MonoidAlgebra` `nonAssocSemiring` `Monoid.toMulOneClass` `RingHom.instFunLike` `mapRangeRingHom` `Finsupp.mapRange` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `NonAssocSemiring.toMulZeroOneClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`	—	—
`commRingEquiv_single_single` 📖	mathematical	—	`DFunLike.coe` `RingEquiv` `MonoidAlgebra` `semiring` `instMul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `nonUnitalNonAssocSemiring` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `commRingEquiv` `single`	—	`Finsupp.uncurry_single` `Finsupp.mapDomain_single` `Finsupp.curry_single`
`mapDomainAddEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instFunLike` `AddEquiv` `MonoidAlgebra` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `nonUnitalNonAssocSemiring` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `mapDomainAddEquiv` `Equiv` `Equiv.instEquivLike` `Equiv.symm`	—	`Finsupp.mapDomain_equiv_apply`
`mapDomainAddEquiv_single` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `MonoidAlgebra` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `nonUnitalNonAssocSemiring` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `mapDomainAddEquiv` `single` `Equiv` `Equiv.instEquivLike`	—	`Finsupp.mapDomain_single`
`mapDomainAddEquiv_trans` 📖	mathematical	—	`mapDomainAddEquiv` `Equiv.trans` `AddEquiv.trans` `MonoidAlgebra` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `nonUnitalNonAssocSemiring`	—	`AddEquiv.ext` `ext` `mapDomainAddEquiv_apply`
`mapDomainNonUnitalRingHom_apply` 📖	mathematical	—	`DFunLike.coe` `NonUnitalRingHom` `MonoidAlgebra` `nonUnitalNonAssocSemiring` `NonUnitalRingHom.instFunLike` `mapDomainNonUnitalRingHom` `mapDomain` `MulHom` `MulHom.funLike`	—	—
`mapDomainNonUnitalRingHom_comp` 📖	mathematical	—	`mapDomainNonUnitalRingHom` `MulHom.comp` `NonUnitalRingHom.comp` `MonoidAlgebra` `nonUnitalNonAssocSemiring`	—	`NonUnitalRingHom.ext` `ext` `Finsupp.mapDomain_comp`
`mapDomainNonUnitalRingHom_id` 📖	mathematical	—	`mapDomainNonUnitalRingHom` `MulHom.id` `NonUnitalRingHom.id` `MonoidAlgebra` `nonUnitalNonAssocSemiring`	—	`NonUnitalRingHom.ext` `ext` `Finsupp.mapDomain_id`
`mapDomainRingEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instFunLike` `RingEquiv` `MonoidAlgebra` `instMul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `nonUnitalNonAssocSemiring` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `mapDomainRingEquiv` `MulEquiv` `MulEquiv.instEquivLike` `MulEquiv.symm`	—	`mapDomainAddEquiv_apply`
`mapDomainRingEquiv_single` 📖	mathematical	—	`DFunLike.coe` `RingEquiv` `MonoidAlgebra` `instMul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `nonUnitalNonAssocSemiring` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `mapDomainRingEquiv` `single` `MulEquiv` `MulEquiv.instEquivLike`	—	`Finsupp.mapDomain_single`
`mapDomainRingEquiv_trans` 📖	mathematical	—	`mapDomainRingEquiv` `MulEquiv.trans` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `RingEquiv.trans` `MonoidAlgebra` `instMul` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `nonUnitalNonAssocSemiring`	—	`RingEquiv.ext` `ext` `mapDomainRingEquiv_apply`
`mapDomainRingHom_apply` 📖	mathematical	—	`DFunLike.coe` `RingHom` `MonoidAlgebra` `nonAssocSemiring` `Monoid.toMulOneClass` `RingHom.instFunLike` `mapDomainRingHom` `mapDomain` `MonoidHom` `MulOneClass.toMulOne` `MonoidHom.instFunLike`	—	—
`mapDomainRingHom_comp` 📖	mathematical	—	`mapDomainRingHom` `MonoidHom.comp` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `RingHom.comp` `MonoidAlgebra` `nonAssocSemiring`	—	`ringHom_ext` `ext` `Finsupp.mapDomain_single` `map_one` `MonoidHomClass.toOneHomClass` `MonoidHom.instMonoidHomClass`
`mapDomainRingHom_id` 📖	mathematical	—	`mapDomainRingHom` `MonoidHom.id` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `RingHom.id` `MonoidAlgebra` `nonAssocSemiring`	—	`ringHom_ext` `ext` `Finsupp.mapDomain_single`
`mapDomain_add` 📖	mathematical	—	`mapDomain` `MonoidAlgebra` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `addCommMonoid`	—	`Finsupp.mapDomain_add`
`mapDomain_injective` 📖	mathematical	—	`MonoidAlgebra` `mapDomain`	—	`Finsupp.mapDomain_injective`
`mapDomain_mul` 📖	mathematical	—	`mapDomain` `DFunLike.coe` `MonoidAlgebra` `instMul`	—	`mul_def` `mapDomain_sum` `Finsupp.mapDomain_single` `map_mul` `Finsupp.sum_mapDomain_index` `MulZeroClass.mul_zero` `Finsupp.single_zero` `mul_add` `Distrib.leftDistribClass` `Finsupp.single_add` `MulZeroClass.zero_mul` `Finsupp.sum_fun_zero` `add_mul` `Distrib.rightDistribClass` `Finsupp.sum_add`
`mapDomain_one` 📖	mathematical	—	`mapDomain` `DFunLike.coe` `MonoidAlgebra` `one`	—	`Finsupp.mapDomain_single` `map_one`
`mapDomain_single` 📖	mathematical	—	`mapDomain` `single`	—	`ext` `Finsupp.mapDomain_single`
`mapDomain_sum` 📖	mathematical	—	`mapDomain` `Finsupp.sum` `MonoidAlgebra` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `addCommMonoid`	—	`Finsupp.mapDomain_sum`
`mapDomain_zero` 📖	mathematical	—	`mapDomain` `MonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `addCommMonoid`	—	`Finsupp.mapDomain_zero`
`mapRangeAddEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instFunLike` `AddEquiv` `MonoidAlgebra` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `nonUnitalNonAssocSemiring` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `mapRangeAddEquiv`	—	—
`mapRangeAddEquiv_single` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `MonoidAlgebra` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `nonUnitalNonAssocSemiring` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `mapRangeAddEquiv` `single` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`Finsupp.mapRange_single`
`mapRangeAddEquiv_trans` 📖	mathematical	—	`mapRangeAddEquiv` `AddEquiv.trans` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `MonoidAlgebra` `nonUnitalNonAssocSemiring`	—	`AddEquiv.ext` `ext` `mapRangeAddEquiv_apply`
`mapRangeRingEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instFunLike` `RingEquiv` `MonoidAlgebra` `instMul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `nonUnitalNonAssocSemiring` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `mapRangeRingEquiv` `Distrib.toMul`	—	`mapRangeRingHom_apply`
`mapRangeRingEquiv_single` 📖	mathematical	—	`DFunLike.coe` `RingEquiv` `MonoidAlgebra` `instMul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `nonUnitalNonAssocSemiring` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `mapRangeRingEquiv` `single` `Distrib.toMul` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`mapRangeRingHom_single`
`mapRangeRingEquiv_trans` 📖	mathematical	—	`mapRangeRingEquiv` `RingEquiv.trans` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toAdd` `MonoidAlgebra` `instMul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `nonUnitalNonAssocSemiring`	—	`RingEquiv.ext` `ext` `mapRangeRingEquiv_apply`
`mapRangeRingHom_apply` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instFunLike` `RingHom` `MonoidAlgebra` `nonAssocSemiring` `Monoid.toMulOneClass` `RingHom.instFunLike` `mapRangeRingHom`	—	—
`mapRangeRingHom_comp` 📖	mathematical	—	`mapRangeRingHom` `RingHom.comp` `Semiring.toNonAssocSemiring` `MonoidAlgebra` `nonAssocSemiring` `Monoid.toMulOneClass`	—	`ringHom_ext` `ext` `mapRangeRingHom_single` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`
`mapRangeRingHom_comp_mapDomainRingHom` 📖	mathematical	—	`RingHom.comp` `MonoidAlgebra` `nonAssocSemiring` `Monoid.toMulOneClass` `mapRangeRingHom` `mapDomainRingHom`	—	`ringHom_ext` `ext` `Finsupp.mapDomain_single` `map_one` `MonoidHomClass.toOneHomClass` `MonoidHom.instMonoidHomClass` `mapRangeRingHom_single` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`
`mapRangeRingHom_id` 📖	mathematical	—	`mapRangeRingHom` `RingHom.id` `Semiring.toNonAssocSemiring` `MonoidAlgebra` `nonAssocSemiring` `Monoid.toMulOneClass`	—	`ringHom_ext` `ext` `mapRangeRingHom_single`
`mapRangeRingHom_single` 📖	mathematical	—	`DFunLike.coe` `RingHom` `MonoidAlgebra` `nonAssocSemiring` `Monoid.toMulOneClass` `RingHom.instFunLike` `mapRangeRingHom` `single` `Semiring.toNonAssocSemiring`	—	`ext` `mapRangeRingHom_apply` `single_apply` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`
`ringHom_ext_iff` 📖	mathematical	—	`DFunLike.coe` `RingHom` `MonoidAlgebra` `nonAssocSemiring` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `single` `MulOne.toOne` `MulOneClass.toMulOne` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`ringHom_ext`
`symm_commRingEquiv` 📖	mathematical	—	`RingEquiv.symm` `MonoidAlgebra` `semiring` `instMul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `nonUnitalNonAssocSemiring` `commRingEquiv`	—	—
`symm_mapDomainAddEquiv` 📖	mathematical	—	`AddEquiv.symm` `MonoidAlgebra` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `nonUnitalNonAssocSemiring` `mapDomainAddEquiv` `Equiv.symm`	—	—
`symm_mapDomainRingEquiv` 📖	mathematical	—	`RingEquiv.symm` `MonoidAlgebra` `instMul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `nonUnitalNonAssocSemiring` `mapDomainRingEquiv` `MulEquiv.symm`	—	—
`symm_mapRangeAddEquiv` 📖	mathematical	—	`AddEquiv.symm` `MonoidAlgebra` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `nonUnitalNonAssocSemiring` `mapRangeAddEquiv` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	—
`symm_mapRangeRingEquiv` 📖	mathematical	—	`RingEquiv.symm` `MonoidAlgebra` `instMul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `nonUnitalNonAssocSemiring` `mapRangeRingEquiv` `Distrib.toMul` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	—
`toRingHom_mapDomainRingEquiv` 📖	mathematical	—	`RingEquiv.toRingHom` `MonoidAlgebra` `nonAssocSemiring` `Monoid.toMulOneClass` `mapDomainRingEquiv` `mapDomainRingHom` `MonoidHomClass.toMonoidHom` `MulEquiv` `MulOne.toMul` `MulOneClass.toMulOne` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `MulEquivClass.instMonoidHomClass` `MulEquiv.instMulEquivClass`	—	—
`toRingHom_mapRangeRingEquiv` 📖	mathematical	—	`RingEquiv.toRingHom` `MonoidAlgebra` `nonAssocSemiring` `Monoid.toMulOneClass` `mapRangeRingEquiv` `mapRangeRingHom` `RingHomClass.toRingHom` `RingEquiv` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass`	—	—

---

← Back to Index