English
Let R be a commutative ring and T a subsemiring of R, together with data mem_of_isSquare and neg_one_notMem that define a ring preordering mk from T. Then for every x ∈ R, x belongs to mk(T, mem_of_isSquare, neg_one_notMem) if and only if x ∈ T.
Русский
Пусть R — коммутативное кольцо, T — подпол semiring кольца R, и имеется соответствующее доказательство mem_of_isSquare и neg_one_notMem, задающее предрасположение mk. Тогда для каждого x ∈ R верно: x ∈ mk(T, mem_of_isSquare, neg_one_notMem) тогда и только тогда, когда x ∈ T.
LaTeX
$$$x \\in \\mathrm{mk}(T,\\mathrm{mem\\_of\\_isSquare},\\mathrm{neg\\_one\\_notMem}) \\iff x \\in T$$$
Lean4
@[simp]
theorem mem_mk {toSubsemiring : Subsemiring R} (mem_of_isSquare neg_one_notMem) {x : R} :
x ∈ mk toSubsemiring mem_of_isSquare neg_one_notMem ↔ x ∈ toSubsemiring :=
.rfl
