mem_subalgebraOfSubsemiring — Mathlib

English

For any x ∈ R and any S ⊆ R that is a Subsemiring, x ∈ subalgebraOfSubsemiring S if and only if x ∈ S.

Русский

Для любого x в R и подполе S, являющемся Subsemiring, верно: x ∈ subalgebraOfSubsemiring S тогда и только тогда, когда x ∈ S.

LaTeX

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

Lean4

@[simp]
theorem mem_subalgebraOfSubsemiring {x : R} {S : Subsemiring R} : x ∈ subalgebraOfSubsemiring S ↔ x ∈ S :=
  Iff.rfl

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