Commit 2023-06-20 15:11 a11e3f3d

View on Github →

feat: port RingTheory.Norm (#5262)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/Norm.lean

added theorem Algebra.PowerBasis.norm_gen_eq_coeff_zero_minpoly

added theorem Algebra.PowerBasis.norm_gen_eq_prod_roots

added theorem Algebra.isIntegral_norm

added theorem Algebra.norm_algebraMap_of_basis

added theorem Algebra.norm_apply

added theorem Algebra.norm_eq_matrix_det

added theorem Algebra.norm_eq_norm_adjoin

added theorem Algebra.norm_eq_one_of_not_exists_basis

added theorem Algebra.norm_eq_one_of_not_module_finite

added theorem Algebra.norm_eq_prod_automorphisms

added theorem Algebra.norm_eq_prod_embeddings

added theorem Algebra.norm_eq_prod_embeddings_gen

added theorem Algebra.norm_eq_prod_roots

added theorem Algebra.norm_eq_zero_iff'

added theorem Algebra.norm_eq_zero_iff

added theorem Algebra.norm_eq_zero_iff_of_basis

added theorem Algebra.norm_ne_zero_iff

added theorem Algebra.norm_ne_zero_iff_of_basis

added theorem Algebra.norm_norm

added theorem Algebra.norm_zero

added theorem Algebra.prod_embeddings_eq_finrank_pow

added theorem IntermediateField.AdjoinSimple.norm_gen_eq_one

added theorem IntermediateField.AdjoinSimple.norm_gen_eq_prod_roots