Commit 2026-06-17 11:02 ce224279

View on Github →

feat: add Algebra.norm_zpow (#40238) We generalize Algebra.norm_inv from fields to division rings and we add Algebra.norm_zpow. From flt-regular.

Estimated changes

Modified Mathlib/RingTheory/Norm/Basic.lean

modified theorem Algebra.norm_inv

added theorem Algebra.norm_zpow