mapValueGroupWithZero_valuation — Mathlib

English

For any a ∈ A, mapValueGroupWithZero A B (valuation _ a) = valuation _ (algebraMap _ _ a).

Русский

Для любого a ∈ A: mapValueGroupWithZero(A,B)(valuation a) = valuation(algebraMap(a)).

LaTeX

$$$\\text{mapValueGroupWithZero}(A,B)(\\mathrm{valuation} _ a) = \\mathrm{valuation} _ (\\mathrm{algebraMap} A B\ n a)$$$

Lean4

@[simp]
theorem mapValueGroupWithZero_valuation (a : A) :
    mapValueGroupWithZero A B (valuation _ a) = valuation _ (algebraMap _ _ a) := by simp [valuation]

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