toSubring — Mathlib

English

A Subsemiring that contains -1 can be upgraded to a Subring.

Русский

Подпол semiring, содержащий −1, становится подкольцом.

LaTeX

$$$$\text{toSubring}(s, h_{neg})\text{ is a Subring of } R,$$$$

Lean4

/-- A `Subsemiring` containing -1 is a `Subring`. -/
@[simps toSubsemiring]
def toSubring (s : Subsemiring R) (hneg : (-1 : R) ∈ s) : Subring R
    where
  toSubsemiring := s
  neg_mem'
    h := by
    rw [← neg_one_mul]
    exact mul_mem hneg h

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