norm_eq_of_algEquiv — Mathlib

English

If e is an R-algebra isomorphism between S and T and x ∈ S, then the norm of e(x) (in T) equals the norm of x (in S).

Русский

Если e — изоморфизм R-алгебр S → T, тогда норма e(x) в T равна норме x в S.

LaTeX

$$$ \\operatorname{norm}_R(e(x)) = \\operatorname{norm}_R(x) $$$

Lean4

theorem norm_eq_of_algEquiv [Ring T] [Algebra R T] (e : S ≃ₐ[R] T) (x) : Algebra.norm R (e x) = Algebra.norm R x := by
  simp_rw [Algebra.norm_apply, ← LinearMap.det_conj _ e.toLinearEquiv]; congr; ext; simp

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