mapOfLE — Mathlib

English

The canonical map on value groups induced by a coarsening of valuation rings.

Русский

Каноническое отображение на группы значений, индуцируемое упрощением оценок колец.

LaTeX

$$$mapOfLE(R,S,h): R.ValueGroup \to*₀ S.ValueGroup$$$

Lean4

/-- The canonical map on value groups induced by a coarsening of valuation rings. -/
def mapOfLE (R S : ValuationSubring K) (h : R ≤ S) : R.ValueGroup →*₀ S.ValueGroup
    where
  toFun := Quotient.map' id fun _ _ ⟨u, hu⟩ => ⟨Units.map (R.inclusion S h).toMonoidHom u, hu⟩
  map_zero' := rfl
  map_one' := rfl
  map_mul' := by rintro ⟨⟩ ⟨⟩; rfl

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