ENatMap — Mathlib

English

A version of ENat.map for MonoidWithZeroHom; ENat.map is extended to ENat(WithTop S) respecting zero.

Русский

Версия ENat.map для MonoidWithZeroHom; ENat.map распространяется на ENat(WithTop S) с учётом нуля.

LaTeX

$$$$ \\text{MonoidWithZeroHom.ENatMap}(f)(n) = \\mathrm{ENat.map}(f)(n) \\quad (n \\in \\mathbb{N}^∞) $$$$

Lean4

/-- A version of `ENat.map` for `MonoidWithZeroHom`s. -/
@[simps -fullyApplied]
protected def _root_.MonoidWithZeroHom.ENatMap {S : Type*} [MulZeroOneClass S] [DecidableEq S] [Nontrivial S]
    (f : ℕ →*₀ S) (hf : Function.Injective f) : ℕ∞ →*₀ WithTop S :=
  { f.toZeroHom.ENatMap,
    f.toMonoidHom.toOneHom.ENatMap with
    toFun := ENat.map f
    map_mul' := fun x y =>
      by
      have : ∀ z, map f z = 0 ↔ z = 0 := fun z => (WithTop.map_injective hf).eq_iff' f.toZeroHom.ENatMap.map_zero
      rcases Decidable.eq_or_ne x 0 with (rfl | hx)
      · simp
      rcases Decidable.eq_or_ne y 0 with (rfl | hy)
      · simp
      induction x with
      | top => simp [hy, this]
      | coe x =>
        induction y with
        | top =>
          have : (f x : WithTop S) ≠ 0 := by simpa [hf.eq_iff' (map_zero f)] using hx
          simp [mul_top hx, WithTop.mul_top this]
        | coe y => simp [← Nat.cast_mul, -coe_mul] }

Похожие утверждения