instCanLiftSetCoeAndMemOfNatForallForallForallForallHAddForallForallForallForallHMulForallForallForallHSMul

English

There is a canonical NonUnitalSubsemiringClass structure on NonUnitalSubalgebra R A.

Русский

Существует каноническая структура NonUnitalSubsemiringClass на NonUnitalSubalgebra R A.

LaTeX

$$NonUnitalSubalgebra.instNonUnitalSubsemiringClass$$

Lean4

instance (priority := 100) :
    CanLift (Set A) (NonUnitalSubalgebra R A) (↑)
      (fun s ↦
        0 ∈ s ∧
          (∀ {x y}, x ∈ s → y ∈ s → x + y ∈ s) ∧
            (∀ {x y}, x ∈ s → y ∈ s → x * y ∈ s) ∧ ∀ (r : R) {x}, x ∈ s → r • x ∈ s)
    where
  prf s
    h :=
    ⟨{  carrier := s
        zero_mem' := h.1
        add_mem' := h.2.1
        mul_mem' := h.2.2.1
        smul_mem' := h.2.2.2 }, rfl⟩

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