mem_mk — Mathlib

English

For any ring R and Subsemiring S, the RingCone mk constructed from S has carrier exactly S, i.e., membership in mk(S) is equivalent to membership in S.

Русский

Для кольца R и подпполусемиринга S конус RingCone, образованный из S, имеет носитель ровно S; членство в mk(S) эквивалентно членству в S.

LaTeX

$$$ x \\in \\mathrm{mk}(toSubsemiring, eq\\_zero\\_of\\_mem\\_of\\_neg\\_mem) \\;\\Leftrightarrow\\; x \\in toSubsemiring. $$$

Lean4

@[simp]
theorem mem_mk {R : Type*} [Ring R] {toSubsemiring : Subsemiring R} (eq_zero_of_mem_of_neg_mem) {x : R} :
    x ∈ mk toSubsemiring eq_zero_of_mem_of_neg_mem ↔ x ∈ toSubsemiring :=
  .rfl

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