Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-07 06:45 0d186304

View on Github →

chore(ring_theory/norm): generalise a couple of lemmas (#15160) Using the generalisation linter

Estimated changes

Modified src/ring_theory/norm.lean

modified theorem algebra.norm_eq_prod_embeddings_gen

modified theorem algebra.norm_eq_zero_iff'

modified theorem algebra.norm_eq_zero_iff

modified theorem algebra.prod_embeddings_eq_finrank_pow