English
Under suitable finiteness and domain hypotheses, the norm of x equals zero if and only if x equals zero.
Русский
При подходящих условиях области и конечности эквивалентно: нормa x = 0 тогда и только тогда, когда x = 0.
LaTeX
$$norm R x = 0 ↔ x = 0$$
Lean4
/-- Given `pb : PowerBasis R S`, then the norm of `pb.gen` is
`((minpoly R pb.gen).aroots F).prod`. -/
theorem norm_gen_eq_prod_roots [Algebra R F] (pb : PowerBasis R S) (hf : (minpoly R pb.gen).Splits (algebraMap R F)) :
algebraMap R F (norm R pb.gen) = ((minpoly R pb.gen).aroots F).prod :=
by
haveI := Module.nontrivial R F
have := minpoly.monic pb.isIntegral_gen
rw [PowerBasis.norm_gen_eq_coeff_zero_minpoly, ← pb.natDegree_minpoly, RingHom.map_mul, ← coeff_map,
coeff_zero_eq_prod_roots_of_monic_of_splits (this.map _) ((splits_id_iff_splits _).2 hf), this.natDegree_map,
map_pow, ← mul_assoc, ← mul_pow]
simp only [map_neg, map_one, neg_mul, neg_neg, one_pow, one_mul]
