Theorems · Definition · order theory
MonoidWithZeroHom.ENatMap
{S : Type u_2} →
[inst : MulZeroOneClass S] →
[inst_1 : DecidableEq S] → [inst_2 : Nontrivial S] → (f : ℕ →*₀ S) → Function.Injective ⇑f → ℕ∞ →*₀ WithTop SA version of ENat.map for MonoidWithZeroHoms.
- Defined in
- Mathlib.Data.ENat.Basic
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 35 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites14
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- ENatstatement and proof · cited by 4,985
- WithTopstatement and proof · cited by 3,754
- Nontrivialstatement and proof · cited by 2,416
- MonoidWithZeroHomstatement and proof · cited by 704
- MulZeroOneClassstatement and proof · cited by 184
- ZeroHomproof · cited by 161
- MonoidHom.toOneHomproof · cited by 132
- OneHomproof · cited by 55
- MonoidWithZeroHom.toMonoidHomproof · cited by 39
- MonoidWithZeroHom.toZeroHomproof · cited by 35
- ENat.mapproof · cited by 31
Cited by4
Results whose statement or proof uses this declaration.
- RingHom.ENatMapproof · cited by 1
- MonoidWithZeroHom.ENatMap_applystatement and proof · cited by 0
- ENat.map_natCast_mulproof · cited by 0
- RingHom.ENatMap_applystatement · cited by 0