English
An absolute value on R can be transported to T via an injective ring homomorphism f: T →+* R, producing an absolute value on T.
Русский
Пусть есть абсолютное значение на R; через инъективное кольцевое гомоморфизмf: T →+* R получаем абсолютное значение на T.
LaTeX
$$AbsoluteValue.comp v f hf$$
Lean4
/-- Construct an absolute value on a semiring `T` from an absolute value on a semiring `R`
and an injective ring homomorphism `f : T →+* R` -/
def comp {R S T : Type*} [Semiring T] [Semiring R] [Semiring S] [PartialOrder S] (v : AbsoluteValue R S) {f : T →+* R}
(hf : Function.Injective f) : AbsoluteValue T S
where
toMulHom := v.1.comp f
nonneg' _ := v.nonneg _
eq_zero' _ := v.eq_zero.trans (map_eq_zero_iff f hf)
add_le' _ _ := (congr_arg v (map_add f _ _)).trans_le (v.add_le _ _)
