MapDomain

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

Statistics

Metric	Count
Definitions `comapDomain`, `comapDomainAddMonoidHom`, `commRingEquiv`, `map`, `mapAddEquiv`, `mapDomain`, `mapDomainAddEquiv`, `mapDomainNonUnitalRingHom`, `mapDomainRingEquiv`, `mapDomainRingHom`, `mapRingEquiv`, `mapRingHom`, `toMultiplicative`, `comapDomain`, `comapDomainAddMonoidHom`, `commRingEquiv`, `map`, `mapAddEquiv`, `mapDomain`, `mapDomainAddEquiv`, `mapDomainNonUnitalRingHom`, `mapDomainRingEquiv`, `mapDomainRingHom`, `mapRangeAddEquiv`, `mapRangeRingEquiv`, `mapRangeRingHom`, `mapRingEquiv`, `mapRingHom`	28
Theorems `coe_mapRingHom`, `coeff_comapDomain`, `coeff_map`, `comapDomainAddMonoidHom_apply`, `comapDomain_add`, `comapDomain_single_map`, `comapDomain_zero`, `commRingEquiv_single_single`, `mapAddEquiv_apply`, `mapAddEquiv_single`, `mapAddEquiv_trans`, `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_comapDomain`, `mapDomain_injective`, `mapDomain_mul`, `mapDomain_one`, `mapDomain_single`, `mapDomain_sum`, `mapDomain_zero`, `mapRingEquiv_apply`, `mapRingEquiv_single`, `mapRingEquiv_trans`, `mapRingHom_apply`, `mapRingHom_comp`, `mapRingHom_comp_mapDomainRingHom`, `mapRingHom_id`, `mapRingHom_single`, `map_add`, `map_id`, `map_map`, `map_mul`, `map_neg`, `map_one`, `map_single`, `map_sub`, `map_sum`, `map_zero`, `ofCoeff_mapRange`, `symm_commRingEquiv`, `symm_mapAddEquiv`, `symm_mapDomainAddEquiv`, `symm_mapDomainRingEquiv`, `symm_mapRingEquiv`, `toRingHom_mapDomainRingEquiv`, `toRingHom_mapRingEquiv`, `coe_mapRangeRingHom`, `coe_mapRingHom`, `coeff_comapDomain`, `coeff_map`, `comapDomainAddMonoidHom_apply`, `comapDomain_add`, `comapDomain_single_map`, `comapDomain_single_of_not_mem_range`, `comapDomain_zero`, `commRingEquiv_single_single`, `mapAddEquiv_apply`, `mapAddEquiv_single`, `mapAddEquiv_trans`, `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_comapDomain`, `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`, `mapRingEquiv_apply`, `mapRingEquiv_single`, `mapRingEquiv_trans`, `mapRingHom_apply`, `mapRingHom_comp`, `mapRingHom_comp_mapDomainRingHom`, `mapRingHom_id`, `mapRingHom_single`, `map_add`, `map_id`, `map_map`, `map_mul`, `map_neg`, `map_one`, `map_single`, `map_sub`, `map_sum`, `map_zero`, `ofCoeff_mapRange`, `ringHom_ext_iff`, `symm_commRingEquiv`, `symm_mapAddEquiv`, `symm_mapDomainAddEquiv`, `symm_mapDomainRingEquiv`, `symm_mapRangeAddEquiv`, `symm_mapRangeRingEquiv`, `symm_mapRingEquiv`, `toRingHom_mapDomainRingEquiv`, `toRingHom_mapRangeRingEquiv`, `toRingHom_mapRingEquiv`	131
Total	159

AddMonoidAlgebra

Definitions

Name	Category	Theorems
`comapDomain` 📖	CompOp	6 math math: `comapDomain_add`, `coeff_comapDomain`, `comapDomainAddMonoidHom_apply`, `mapDomain_comapDomain`, `comapDomain_zero`, `comapDomain_single_map`
`comapDomainAddMonoidHom` 📖	CompOp	1 math math: `comapDomainAddMonoidHom_apply`
`commRingEquiv` 📖	CompOp	2 math math: `commRingEquiv_single_single`, `symm_commRingEquiv`
`map` 📖	CompOp	13 math math: `map_map`, `map_single`, `map_sub`, `coe_mapRingHom`, `ofCoeff_mapRange`, `map_id`, `map_add`, `map_one`, `map_neg`, `map_sum`, `map_zero`, `map_mul`, `coeff_map`
`mapAddEquiv` 📖	CompOp	4 math math: `mapAddEquiv_single`, `mapAddEquiv_apply`, `symm_mapAddEquiv`, `mapAddEquiv_trans`
`mapDomain` 📖	CompOp	14 math math: `mapDomain_one`, `mapDomainNonUnitalRingHom_apply`, `mapDomainBialgHom_apply`, `Polynomial.toLaurent_apply`, `mapDomainAlgHom_apply`, `mapDomain_comapDomain`, `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`, `mapDomainRingHom_apply`, `mapRingHom_comp_mapDomainRingHom`
`mapRingEquiv` 📖	CompOp	5 math math: `toRingHom_mapRingEquiv`, `mapRingEquiv_apply`, `symm_mapRingEquiv`, `mapRingEquiv_trans`, `mapRingEquiv_single`
`mapRingHom` 📖	CompOp	12 math math: `lift_mapRangeRingHom_algebraMap`, `toRingHom_mapAlgHom`, `algebraMap_def`, `mapRingHom_id`, `mapRingHom_comp_algebraMap`, `coe_mapRingHom`, `toRingHom_mapRingEquiv`, `mapRingHom_single`, `lift_mapRingHom_algebraMap`, `mapRingHom_apply`, `mapRingHom_comp`, `mapRingHom_comp_mapDomainRingHom`
`toMultiplicative` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_mapRingHom` 📖	mathematical	—	`DFunLike.coe` `RingHom` `AddMonoidAlgebra` `nonAssocSemiring` `AddMonoid.toAddZeroClass` `RingHom.instFunLike` `mapRingHom` `map` `AddMonoidHomClass.toAddMonoidHom` `Semiring.toNonAssocSemiring` `AddZeroClass.toAddZero` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass`	—	—
`coeff_comapDomain` 📖	mathematical	—	`coeff` `comapDomain` `Finsupp.comapDomain` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Function.Injective.injOn` `Set.preimage` `SetLike.coe` `Finset` `Finset.instSetLike` `Finsupp.support`	—	—
`coeff_map` 📖	mathematical	—	`coeff` `map` `Finsupp.mapRange` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `DFunLike.coe` `AddMonoidHom` `AddMonoidHom.instFunLike` `AddMonoidHom.map_zero`	—	—
`comapDomainAddMonoidHom_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddMonoidAlgebra` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `addAddCommMonoid` `AddMonoidHom.instFunLike` `comapDomainAddMonoidHom` `comapDomain`	—	—
`comapDomain_add` 📖	mathematical	—	`comapDomain` `AddMonoidAlgebra` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `addAddCommMonoid`	—	`Function.Injective.injOn` `Finsupp.comapDomain_add_of_injective`
`comapDomain_single_map` 📖	mathematical	—	`comapDomain` `single`	—	`Finsupp.comapDomain_single`
`comapDomain_zero` 📖	mathematical	—	`comapDomain` `AddMonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `addAddCommMonoid`	—	`Finsupp.comapDomain_zero`
`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`
`mapAddEquiv_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` `mapAddEquiv`	—	—
`mapAddEquiv_single` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `AddMonoidAlgebra` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `nonUnitalNonAssocSemiring` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `mapAddEquiv` `single` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`map_single`
`mapAddEquiv_trans` 📖	mathematical	—	`mapAddEquiv` `AddEquiv.trans` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddMonoidAlgebra` `nonUnitalNonAssocSemiring`	—	`AddEquiv.ext` `ext` `mapAddEquiv_apply`
`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_comapDomain` 📖	mathematical	`Set` `Set.instHasSubset` `SetLike.coe` `Finset` `Finset.instSetLike` `Finsupp.support` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `coeff` `Set.range`	`mapDomain` `comapDomain`	—	`Finsupp.mapDomain_comapDomain`
`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`
`mapRingEquiv_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` `mapRingEquiv` `Distrib.toMul`	—	`mapRingHom_apply`
`mapRingEquiv_single` 📖	mathematical	—	`DFunLike.coe` `RingEquiv` `AddMonoidAlgebra` `instMul` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `nonUnitalNonAssocSemiring` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `mapRingEquiv` `single` `Distrib.toMul` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`mapRingHom_single`
`mapRingEquiv_trans` 📖	mathematical	—	`mapRingEquiv` `RingEquiv.trans` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toAdd` `AddMonoidAlgebra` `instMul` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `nonUnitalNonAssocSemiring`	—	`RingEquiv.ext` `ext` `mapRingEquiv_apply`
`mapRingHom_apply` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instFunLike` `RingHom` `AddMonoidAlgebra` `nonAssocSemiring` `AddMonoid.toAddZeroClass` `RingHom.instFunLike` `mapRingHom`	—	—
`mapRingHom_comp` 📖	mathematical	—	`mapRingHom` `RingHom.comp` `Semiring.toNonAssocSemiring` `AddMonoidAlgebra` `nonAssocSemiring` `AddMonoid.toAddZeroClass`	—	`ringHom_ext` `ext` `mapRingHom_single` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`
`mapRingHom_comp_mapDomainRingHom` 📖	mathematical	—	`RingHom.comp` `AddMonoidAlgebra` `nonAssocSemiring` `AddMonoid.toAddZeroClass` `mapRingHom` `mapDomainRingHom`	—	`ringHom_ext` `ext` `Finsupp.mapDomain_single` `map_zero` `AddMonoidHomClass.toZeroHomClass` `AddMonoidHom.instAddMonoidHomClass` `mapRingHom_single` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`
`mapRingHom_id` 📖	mathematical	—	`mapRingHom` `RingHom.id` `Semiring.toNonAssocSemiring` `AddMonoidAlgebra` `nonAssocSemiring` `AddMonoid.toAddZeroClass`	—	`ringHom_ext` `ext` `mapRingHom_single`
`mapRingHom_single` 📖	mathematical	—	`DFunLike.coe` `RingHom` `AddMonoidAlgebra` `nonAssocSemiring` `AddMonoid.toAddZeroClass` `RingHom.instFunLike` `mapRingHom` `single` `Semiring.toNonAssocSemiring`	—	`ext` `mapRingHom_apply` `single_apply` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`
`map_add` 📖	mathematical	—	`map` `AddMonoidAlgebra` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `addAddCommMonoid`	—	`Finsupp.mapRange_add` `AddMonoidHom.map_zero` `AddMonoidHom.map_add`
`map_id` 📖	mathematical	—	`map` `AddMonoidHom.id` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring`	—	`Finsupp.mapRange_id`
`map_map` 📖	mathematical	—	`map` `AddMonoidHom.comp` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring`	—	`Finsupp.mapRange_mapRange`
`map_mul` 📖	mathematical	—	`map` `AddMonoidHomClass.toAddMonoidHom` `RingHom` `Semiring.toNonAssocSemiring` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `RingHom.instFunLike` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `AddMonoidAlgebra` `instMul`	—	`ext` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `mul_def` `Finsupp.sum_apply` `single_apply` `map_finsuppSum` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `Finsupp.sum_mapRange_index` `MulZeroClass.mul_zero` `Finsupp.single_zero` `MulZeroClass.zero_mul` `Finsupp.sum_fun_zero`
`map_neg` 📖	mathematical	—	`map` `Ring.toSemiring` `AddMonoidAlgebra` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `addAddCommGroup`	—	`Finsupp.mapRange_neg` `AddMonoidHom.map_zero` `AddMonoidHom.map_neg`
`map_one` 📖	mathematical	—	`map` `AddMonoidHomClass.toAddMonoidHom` `RingHom` `Semiring.toNonAssocSemiring` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `RingHom.instFunLike` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `AddMonoidAlgebra` `zero` `AddZero.toZero`	—	`ext` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `map_single` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass`
`map_single` 📖	mathematical	—	`map` `single` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `AddMonoidHom.instFunLike`	—	`Finsupp.mapRange_single` `AddMonoidHom.map_zero`
`map_sub` 📖	mathematical	—	`map` `Ring.toSemiring` `AddMonoidAlgebra` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `addAddCommGroup`	—	`Finsupp.mapRange_sub` `AddMonoidHom.map_zero` `AddMonoidHom.map_sub`
`map_sum` 📖	mathematical	—	`map` `Finset.sum` `AddMonoidAlgebra` `addAddCommMonoid`	—	`Finsupp.mapRange_finset_sum` `AddMonoidHom.instAddMonoidHomClass`
`map_zero` 📖	mathematical	—	`map` `AddMonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `addAddCommMonoid`	—	`Finsupp.mapRange_zero` `AddMonoidHom.map_zero`
`ofCoeff_mapRange` 📖	mathematical	—	`ofCoeff` `Finsupp.mapRange` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `DFunLike.coe` `AddMonoidHom` `AddMonoidHom.instFunLike` `AddMonoidHom.map_zero` `map`	—	`AddMonoidHom.map_zero`
`symm_commRingEquiv` 📖	mathematical	—	`RingEquiv.symm` `AddMonoidAlgebra` `semiring` `instMul` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `nonUnitalNonAssocSemiring` `commRingEquiv`	—	—
`symm_mapAddEquiv` 📖	mathematical	—	`AddEquiv.symm` `AddMonoidAlgebra` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `nonUnitalNonAssocSemiring` `mapAddEquiv` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	—
`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_mapRingEquiv` 📖	mathematical	—	`RingEquiv.symm` `AddMonoidAlgebra` `instMul` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `nonUnitalNonAssocSemiring` `mapRingEquiv` `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_mapRingEquiv` 📖	mathematical	—	`RingEquiv.toRingHom` `AddMonoidAlgebra` `nonAssocSemiring` `AddMonoid.toAddZeroClass` `mapRingEquiv` `mapRingHom` `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
`comapDomain` 📖	CompOp	7 math math: `comapDomain_single_map`, `mapDomain_comapDomain`, `coeff_comapDomain`, `comapDomain_single_of_not_mem_range`, `comapDomain_add`, `comapDomain_zero`, `comapDomainAddMonoidHom_apply`
`comapDomainAddMonoidHom` 📖	CompOp	1 math math: `comapDomainAddMonoidHom_apply`
`commRingEquiv` 📖	CompOp	2 math math: `symm_commRingEquiv`, `commRingEquiv_single_single`
`map` 📖	CompOp	14 math math: `ofCoeff_mapRange`, `map_one`, `coe_mapRangeRingHom`, `map_zero`, `map_single`, `map_map`, `map_id`, `coeff_map`, `map_sub`, `map_mul`, `map_add`, `map_neg`, `map_sum`, `coe_mapRingHom`
`mapAddEquiv` 📖	CompOp	8 math math: `symm_mapAddEquiv`, `mapAddEquiv_trans`, `mapRangeAddEquiv_apply`, `mapRangeAddEquiv_trans`, `symm_mapRangeAddEquiv`, `mapAddEquiv_apply`, `mapAddEquiv_single`, `mapRangeAddEquiv_single`
`mapDomain` 📖	CompOp	13 math math: `mapDomain_comapDomain`, `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	8 math math: `mapDomainRingHom_id`, `mapRangeRingHom_comp_mapDomainRingHom`, `mapRingHom_comp_mapDomainRingHom`, `toRingHom_mapDomainRingEquiv`, `CommRingCat.monoidAlgebra_map`, `mapDomainRingHom_comp`, `mapDomainRingHom_apply`, `mapDomainRingHom_comp_algebraMap`
`mapRangeAddEquiv` 📖	CompOp	—
`mapRangeRingEquiv` 📖	CompOp	—
`mapRangeRingHom` 📖	CompOp	—
`mapRingEquiv` 📖	CompOp	10 math math: `mapRingEquiv_single`, `mapRangeRingEquiv_single`, `symm_mapRangeRingEquiv`, `toRingHom_mapRingEquiv`, `mapRingEquiv_trans`, `mapRingEquiv_apply`, `mapRangeRingEquiv_apply`, `mapRangeRingEquiv_trans`, `symm_mapRingEquiv`, `toRingHom_mapRangeRingEquiv`
`mapRingHom` 📖	CompOp	21 math math: `mapRangeRingHom_single`, `mapRingHom_apply`, `mapRingHom_comp`, `toRingHom_mapRangeAlgHom`, `coe_mapRangeRingHom`, `toRingHom_mapRingEquiv`, `mapRangeRingHom_comp_mapDomainRingHom`, `mapRingHom_comp_mapDomainRingHom`, `mapRangeRingHom_comp_algebraMap`, `mapRingHom_id`, `algebraMap_def`, `lift_mapRangeRingHom_algebraMap`, `mapRingHom_single`, `lift_mapRingHom_algebraMap`, `toRingHom_mapRangeRingEquiv`, `mapRingHom_comp_algebraMap`, `mapRangeRingHom_id`, `mapRangeRingHom_comp`, `toRingHom_mapAlgHom`, `mapRangeRingHom_apply`, `coe_mapRingHom`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_mapRangeRingHom` 📖	mathematical	—	`DFunLike.coe` `RingHom` `MonoidAlgebra` `nonAssocSemiring` `Monoid.toMulOneClass` `RingHom.instFunLike` `mapRingHom` `map` `AddMonoidHomClass.toAddMonoidHom` `Semiring.toNonAssocSemiring` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass`	—	`coe_mapRingHom`
`coe_mapRingHom` 📖	mathematical	—	`DFunLike.coe` `RingHom` `MonoidAlgebra` `nonAssocSemiring` `Monoid.toMulOneClass` `RingHom.instFunLike` `mapRingHom` `map` `AddMonoidHomClass.toAddMonoidHom` `Semiring.toNonAssocSemiring` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass`	—	—
`coeff_comapDomain` 📖	mathematical	—	`coeff` `comapDomain` `Finsupp.comapDomain` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Function.Injective.injOn` `Set.preimage` `SetLike.coe` `Finset` `Finset.instSetLike` `Finsupp.support`	—	—
`coeff_map` 📖	mathematical	—	`coeff` `map` `Finsupp.mapRange` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `DFunLike.coe` `AddMonoidHom` `AddMonoidHom.instFunLike` `AddMonoidHom.map_zero`	—	—
`comapDomainAddMonoidHom_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `MonoidAlgebra` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `addCommMonoid` `AddMonoidHom.instFunLike` `comapDomainAddMonoidHom` `comapDomain`	—	—
`comapDomain_add` 📖	mathematical	—	`comapDomain` `MonoidAlgebra` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `addCommMonoid`	—	`Function.Injective.injOn` `Finsupp.comapDomain_add_of_injective`
`comapDomain_single_map` 📖	mathematical	—	`comapDomain` `single`	—	`Finsupp.comapDomain_single`
`comapDomain_single_of_not_mem_range` 📖	mathematical	`Set` `Set.instMembership` `Set.range`	`comapDomain` `single` `MonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `addCommMonoid`	—	`Finsupp.comapDomain_single_of_not_mem_range`
`comapDomain_zero` 📖	mathematical	—	`comapDomain` `MonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `addCommMonoid`	—	`Finsupp.comapDomain_zero`
`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`
`mapAddEquiv_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` `mapAddEquiv`	—	—
`mapAddEquiv_single` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `MonoidAlgebra` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `nonUnitalNonAssocSemiring` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `mapAddEquiv` `single` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`map_single`
`mapAddEquiv_trans` 📖	mathematical	—	`mapAddEquiv` `AddEquiv.trans` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `MonoidAlgebra` `nonUnitalNonAssocSemiring`	—	`AddEquiv.ext` `ext` `mapAddEquiv_apply`
`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_comapDomain` 📖	mathematical	`Set` `Set.instHasSubset` `SetLike.coe` `Finset` `Finset.instSetLike` `Finsupp.support` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `coeff` `Set.range`	`mapDomain` `comapDomain`	—	`Finsupp.mapDomain_comapDomain`
`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` `mapAddEquiv`	—	`mapAddEquiv_apply`
`mapRangeAddEquiv_single` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `MonoidAlgebra` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `nonUnitalNonAssocSemiring` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `mapAddEquiv` `single` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`mapAddEquiv_single`
`mapRangeAddEquiv_trans` 📖	mathematical	—	`mapAddEquiv` `AddEquiv.trans` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `MonoidAlgebra` `nonUnitalNonAssocSemiring`	—	`mapAddEquiv_trans`
`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` `mapRingEquiv` `Distrib.toMul`	—	`mapRingEquiv_apply`
`mapRangeRingEquiv_single` 📖	mathematical	—	`DFunLike.coe` `RingEquiv` `MonoidAlgebra` `instMul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `nonUnitalNonAssocSemiring` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `mapRingEquiv` `single` `Distrib.toMul` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`mapRingEquiv_single`
`mapRangeRingEquiv_trans` 📖	mathematical	—	`mapRingEquiv` `RingEquiv.trans` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toAdd` `MonoidAlgebra` `instMul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `nonUnitalNonAssocSemiring`	—	`mapRingEquiv_trans`
`mapRangeRingHom_apply` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instFunLike` `RingHom` `MonoidAlgebra` `nonAssocSemiring` `Monoid.toMulOneClass` `RingHom.instFunLike` `mapRingHom`	—	`mapRingHom_apply`
`mapRangeRingHom_comp` 📖	mathematical	—	`mapRingHom` `RingHom.comp` `Semiring.toNonAssocSemiring` `MonoidAlgebra` `nonAssocSemiring` `Monoid.toMulOneClass`	—	`mapRingHom_comp`
`mapRangeRingHom_comp_mapDomainRingHom` 📖	mathematical	—	`RingHom.comp` `MonoidAlgebra` `nonAssocSemiring` `Monoid.toMulOneClass` `mapRingHom` `mapDomainRingHom`	—	`mapRingHom_comp_mapDomainRingHom`
`mapRangeRingHom_id` 📖	mathematical	—	`mapRingHom` `RingHom.id` `Semiring.toNonAssocSemiring` `MonoidAlgebra` `nonAssocSemiring` `Monoid.toMulOneClass`	—	`mapRingHom_id`
`mapRangeRingHom_single` 📖	mathematical	—	`DFunLike.coe` `RingHom` `MonoidAlgebra` `nonAssocSemiring` `Monoid.toMulOneClass` `RingHom.instFunLike` `mapRingHom` `single` `Semiring.toNonAssocSemiring`	—	`mapRingHom_single`
`mapRingEquiv_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` `mapRingEquiv` `Distrib.toMul`	—	`mapRingHom_apply`
`mapRingEquiv_single` 📖	mathematical	—	`DFunLike.coe` `RingEquiv` `MonoidAlgebra` `instMul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `nonUnitalNonAssocSemiring` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `mapRingEquiv` `single` `Distrib.toMul` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`mapRingHom_single`
`mapRingEquiv_trans` 📖	mathematical	—	`mapRingEquiv` `RingEquiv.trans` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toAdd` `MonoidAlgebra` `instMul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `nonUnitalNonAssocSemiring`	—	`RingEquiv.ext` `ext` `mapRingEquiv_apply`
`mapRingHom_apply` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instFunLike` `RingHom` `MonoidAlgebra` `nonAssocSemiring` `Monoid.toMulOneClass` `RingHom.instFunLike` `mapRingHom`	—	—
`mapRingHom_comp` 📖	mathematical	—	`mapRingHom` `RingHom.comp` `Semiring.toNonAssocSemiring` `MonoidAlgebra` `nonAssocSemiring` `Monoid.toMulOneClass`	—	`ringHom_ext` `ext` `mapRingHom_single` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`
`mapRingHom_comp_mapDomainRingHom` 📖	mathematical	—	`RingHom.comp` `MonoidAlgebra` `nonAssocSemiring` `Monoid.toMulOneClass` `mapRingHom` `mapDomainRingHom`	—	`ringHom_ext` `ext` `Finsupp.mapDomain_single` `map_one` `MonoidHomClass.toOneHomClass` `MonoidHom.instMonoidHomClass` `mapRingHom_single` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`
`mapRingHom_id` 📖	mathematical	—	`mapRingHom` `RingHom.id` `Semiring.toNonAssocSemiring` `MonoidAlgebra` `nonAssocSemiring` `Monoid.toMulOneClass`	—	`ringHom_ext` `ext` `mapRingHom_single`
`mapRingHom_single` 📖	mathematical	—	`DFunLike.coe` `RingHom` `MonoidAlgebra` `nonAssocSemiring` `Monoid.toMulOneClass` `RingHom.instFunLike` `mapRingHom` `single` `Semiring.toNonAssocSemiring`	—	`ext` `mapRingHom_apply` `single_apply` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`
`map_add` 📖	mathematical	—	`map` `MonoidAlgebra` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `addCommMonoid`	—	`Finsupp.mapRange_add` `AddMonoidHom.map_zero` `AddMonoidHom.map_add`
`map_id` 📖	mathematical	—	`map` `AddMonoidHom.id` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring`	—	`Finsupp.mapRange_id`
`map_map` 📖	mathematical	—	`map` `AddMonoidHom.comp` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring`	—	`Finsupp.mapRange_mapRange`
`map_mul` 📖	mathematical	—	`map` `AddMonoidHomClass.toAddMonoidHom` `RingHom` `Semiring.toNonAssocSemiring` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `RingHom.instFunLike` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `MonoidAlgebra` `instMul`	—	`ext` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `mul_def` `Finsupp.sum_apply` `single_apply` `map_finsuppSum` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `Finsupp.sum_mapRange_index` `MulZeroClass.mul_zero` `Finsupp.single_zero` `MulZeroClass.zero_mul` `Finsupp.sum_fun_zero`
`map_neg` 📖	mathematical	—	`map` `Ring.toSemiring` `MonoidAlgebra` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `addCommGroup`	—	`Finsupp.mapRange_neg` `AddMonoidHom.map_zero` `AddMonoidHom.map_neg`
`map_one` 📖	mathematical	—	`map` `AddMonoidHomClass.toAddMonoidHom` `RingHom` `Semiring.toNonAssocSemiring` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `RingHom.instFunLike` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `MonoidAlgebra` `one` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	`ext` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `map_single` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass`
`map_single` 📖	mathematical	—	`map` `single` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `AddMonoidHom.instFunLike`	—	`Finsupp.mapRange_single` `AddMonoidHom.map_zero`
`map_sub` 📖	mathematical	—	`map` `Ring.toSemiring` `MonoidAlgebra` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `addCommGroup`	—	`Finsupp.mapRange_sub` `AddMonoidHom.map_zero` `AddMonoidHom.map_sub`
`map_sum` 📖	mathematical	—	`map` `Finset.sum` `MonoidAlgebra` `addCommMonoid`	—	`Finsupp.mapRange_finset_sum` `AddMonoidHom.instAddMonoidHomClass`
`map_zero` 📖	mathematical	—	`map` `MonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `addCommMonoid`	—	`Finsupp.mapRange_zero` `AddMonoidHom.map_zero`
`ofCoeff_mapRange` 📖	mathematical	—	`ofCoeff` `Finsupp.mapRange` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `DFunLike.coe` `AddMonoidHom` `AddMonoidHom.instFunLike` `AddMonoidHom.map_zero` `map`	—	`AddMonoidHom.map_zero`
`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_mapAddEquiv` 📖	mathematical	—	`AddEquiv.symm` `MonoidAlgebra` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `nonUnitalNonAssocSemiring` `mapAddEquiv` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	—
`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` `mapAddEquiv` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`symm_mapAddEquiv`
`symm_mapRangeRingEquiv` 📖	mathematical	—	`RingEquiv.symm` `MonoidAlgebra` `instMul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `nonUnitalNonAssocSemiring` `mapRingEquiv` `Distrib.toMul` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`symm_mapRingEquiv`
`symm_mapRingEquiv` 📖	mathematical	—	`RingEquiv.symm` `MonoidAlgebra` `instMul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `nonUnitalNonAssocSemiring` `mapRingEquiv` `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` `mapRingEquiv` `mapRingHom` `RingHomClass.toRingHom` `RingEquiv` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass`	—	`toRingHom_mapRingEquiv`
`toRingHom_mapRingEquiv` 📖	mathematical	—	`RingEquiv.toRingHom` `MonoidAlgebra` `nonAssocSemiring` `Monoid.toMulOneClass` `mapRingEquiv` `mapRingHom` `RingHomClass.toRingHom` `RingEquiv` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass`	—	—

---

← Back to Index