English
Let R be a ring and S a seminormed ring, with a ring homomorphism f: R → S. If the norm on R is the one induced by f from S, then ‖1_R‖ = 1 whenever ‖1_S‖ = 1.
Русский
Пусть R — кольцо, S — полуприбранное кольцо (seminormed ring), и есть кольцо-гомоморфизм f: R → S. Если норма на R задаётся индуцированной нормой через f, то ‖1_R‖ = 1 тогда, когда ‖1_S‖ = 1.
LaTeX
$$$\\|1_R\\| = 1$ whenever $\\|1_S\\| = 1$, for the norm on $R$ defined by $\\|x\\|_R = \\|f(x)\\|_S$.$$
Lean4
/-- A ring homomorphism from a `Ring R` to a `SeminormedRing S` which induces the norm structure
`SeminormedRing.induced` makes `R` satisfy `‖(1 : R)‖ = 1` whenever `‖(1 : S)‖ = 1`. -/
theorem induced {F : Type*} (R S : Type*) [Ring R] [SeminormedRing S] [NormMulClass S] [FunLike F R S]
[RingHomClass F R S] (f : F) : @NormMulClass R (SeminormedRing.induced R S f).toNorm _ :=
let _ : SeminormedRing R := SeminormedRing.induced R S f
{ norm_mul x y := (congr_arg norm (map_mul f x y)).trans <| norm_mul _ _ }
