English
If a ring homomorphism into a normed ring induces a norm structure, then the domain has NormOneClass with norm(1)=1.
Русский
Если гомоморфизм кольца в нормированное кольцо индуцирует норму, то область определения имеет NormOneClass с norm(1)=1.
LaTeX
$$$\\text{NormOneClass.induced}\\;R\\;S\\;f=f\\;\\Rightarrow\\; \\|1_{R}\\|=1$$$
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] [NormOneClass S] [FunLike F R S]
[RingHomClass F R S] (f : F) : @NormOneClass R (SeminormedRing.induced R S f).toNorm _ :=
let _ : SeminormedRing R := SeminormedRing.induced R S f
{ norm_one := (congr_arg norm (map_one f)).trans norm_one }
