subsemiringClosure — Mathlib

English

Reiterating the equivalence between map and comap under symmetry of a semiring isomorphism.

Русский

Повторяется эквивалентность между отображением и обратным отображением относительно симметрии изоморфизма полусемиринга.

LaTeX

$$$K.map f = K.comap f.symm$$$

Lean4

/-- The additive closure of a submonoid is a subsemiring. -/
def subsemiringClosure (M : Submonoid R) : Subsemiring R :=
  {
    AddSubmonoid.closure
      (M : Set R) with
    one_mem' := AddSubmonoid.mem_closure.mpr fun _ hy => hy M.one_mem
    mul_mem' := MulMemClass.mul_mem_add_closure }

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