Algebra.norm_prod
Source context 2 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Algebra_norm_prodLean source · statement
theorem _root_.Algebra.norm_prod {R A B : Type*} [CommRing R] [Ring A] [Ring B] [Algebra R A]
[Algebra R B] [Module.Free R A] [Module.Finite R A] [Module.Free R B] [Module.Finite R B] (x : A
× B) : Algebra.norm R x = Algebra.norm R x.1 * Algebra.norm R x.2