Theorems · Definition · ring theory
Algebra.cast
{R : Type u_1} → {A : Type u_2} → [inst : CommSemiring R] → [inst_1 : Semiring A] → [Algebra R A] → R → ACoercion from a commutative semiring to an algebra over this semiring.
- Defined in
- Mathlib.Algebra.Algebra.Defs
- Cited by
- 58 results in Mathlib
- Foundations
- Depth 16 from the axioms · uses no axioms
- Assumes
- CommSemiringSemiringAlgebra
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
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
- Algebrastatement and proof · cited by 11,388
- CommSemiringstatement and proof · cited by 10,911
- Algebra.algebraMapproof · cited by 4,706
Cited by62
Results whose statement or proof uses this declaration.
- RCLike.ofRealproof · cited by 350
- IsDedekindDomain.HeightOneSpectrum.valuation_of_algebraMapstatement and proof · cited by 23
- IsDedekindDomain.HeightOneSpectrum.valuation_le_onestatement · cited by 9
- algebraMap.coe_mulstatement · cited by 7
- algebraMap.coe_onestatement · cited by 7
- SameRay.sameRay_nonneg_smul_rightproof · cited by 6
- algebraMap.coe_zerostatement · cited by 5
- IsGaloisGroup.of_isFractionRingproof · cited by 5
- Submodule.starProjection_singletonproof · cited by 4
- algebraMap.coe_natCaststatement · cited by 4
- algebraMap.coe_powstatement · cited by 4
- IsDedekindDomain.HeightOneSpectrum.valuation_lt_one_iff_memstatement · cited by 3