mem_nonUnitalSubalgebraOfNonUnitalSubsemiring

English

For any S, the membership in the constructed ℕ-subalgebra coincides with membership in S: x lies in nonUnitalSubalgebraOfNonUnitalSubsemiring S if and only if x ∈ S.

Русский

Для любого S принадлежность элемента к сконструированной ℕ-подалгебраической структуре совпадает с принадлежностью к S: x ∈ nonUnitalSubalgebraOfNonUnitalSubsemiring S тогда и только тогда, когда x ∈ S.

LaTeX

$$$x \\in \\operatorname{nonUnitalSubalgebraOfNonUnitalSubsemiring}(S) \\iff x \\in S$$$

Lean4

@[simp]
theorem mem_nonUnitalSubalgebraOfNonUnitalSubsemiring {x : R} {S : NonUnitalSubsemiring R} :
    x ∈ nonUnitalSubalgebraOfNonUnitalSubsemiring S ↔ x ∈ S :=
  Iff.rfl

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