Theorems · Definition · commutative algebra
Nat.castRingHom
(α : Type u_1) → [inst : NonAssocSemiring α] → ℕ →+* α
Nat.cast : ℕ → α as a RingHom
- Defined in
- Mathlib.Data.Nat.Cast.Basic
- Cited by
- 27 results in Mathlib
- Foundations
- Depth 23 from the axioms · uses propext
- Assumes
- NonAssocSemiring
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.
- RingHomstatement · cited by 10,189
- AddMonoidHomproof · cited by 3,230
- NonAssocSemiringstatement and proof · cited by 805
- Nat.cast_mulproof · cited by 309
- Nat.castAddMonoidHomproof · cited by 16
Cited by29
Results whose statement or proof uses this declaration.
- Nat.cast_prodproof · cited by 15
- Finset.prod_natCastproof · cited by 8
- Int.ofNatHomproof · cited by 6
- ENat.toENNRealRingHomproof · cited by 6
- Nat.cast_dvd_castproof · cited by 3
- Polynomial.coprime_of_root_cyclotomicstatement and proof · cited by 2
- Odd.natCastproof · cited by 2
- Fin.isAddFreimanIso_Iicproof · cited by 1
- Nat.cast_list_prodproof · cited by 1
- Nat.coe_castRingHomstatement · cited by 1
- Nat.exists_prime_gt_modEq_oneproof · cited by 1
- MonoidWithZeroHomClass.ext_nnratstatement and proof · cited by 1