castFreeCommRing — Mathlib

English

There exists a finite set s of α (as a Finset) such that IsSupported(x, s).

Русский

Существует конечный набор α (как Finset), для которого IsSupported(x, s).

LaTeX

$$$\\exists s : Finset\\, \\alpha, \\mathrm{IsSupported}(x, (s : Set\\, \\alpha))$$$

Lean4

/-- The coercion defined by the canonical ring homomorphism from the free ring generated by `α` to
the free commutative ring generated by `α`. -/
@[coe]
def castFreeCommRing {α} : FreeRing α → FreeCommRing α :=
  toFreeCommRing

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