Theorems · Theorem · ring theory
AddMonoidAlgebra.mapDomain_single
∀ {R : Type u_3} {M : Type u_6} {N : Type u_7} [inst : Semiring R] {f : M → N} {a : M} {r : R},
AddMonoidAlgebra.mapDomain f (AddMonoidAlgebra.single a r) = AddMonoidAlgebra.single (f a) r- Defined in
- Mathlib.Algebra.MonoidAlgebra.MapDomain
- Cited by
- 23 results in Mathlib
- Foundations
- Depth 73 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- Semiring
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Semiringstatement and proof · cited by 13,802
- Finsupp.singleproof · cited by 943
- AddMonoidAlgebrastatement · cited by 649
- Finsupp.extproof · cited by 399
- AddMonoidAlgebra.singlestatement and proof · cited by 250
- AddMonoidAlgebra.extproof · cited by 90
- Finsupp.mapDomain_singleproof · cited by 48
- AddMonoidAlgebra.mapDomainstatement · cited by 17
- AddMonoidAlgebra.coeff_mapDomainproof · cited by 9
Cited by23
Results whose statement or proof uses this declaration.
- MvPolynomial.rename_Xproof · cited by 48
- AddMonoidAlgebra.mapDomainRingEquiv_singleproof · cited by 6
- MvPolynomial.rename_Cproof · cited by 6
- MvPolynomial.rename_monomialproof · cited by 5
- Polynomial.toLaurent_C_mul_Tproof · cited by 4
- MvPolynomial.tensorEquivSum_X_tmul_oneproof · cited by 3
- MvPolynomial.tensorEquivSum_one_tmul_Xproof · cited by 3
- AddMonoidAlgebra.mapDomainAddEquiv_singleproof · cited by 3
- AddMonoidAlgebra.mapDomainBialgHom_singleproof · cited by 3
- MvPolynomial.tensorEquivSum_X_tmul_Xproof · cited by 2
- MvPolynomial.tensorEquivSum_C_tmul_oneproof · cited by 1
- AddMonoidAlgebra.mapDomainAlgHom_compproof · cited by 1