Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-18 16:08 a0ff65df

View on Github →

feat(ring_theory/norm): add is_integral_norm (#11489) We add is_integral_norm. From flt-regular

Estimated changes

Modified src/ring_theory/norm.lean

added theorem algebra.is_integral_norm

added theorem algebra.norm_eq_prod_roots

modified theorem algebra.prod_embeddings_eq_finrank_pow

added theorem intermediate_field.adjoin_simple.norm_gen_eq_one

added theorem intermediate_field.adjoin_simple.norm_gen_eq_prod_roots