Theorem Algebra.norm_inv

Modification history

2026-06-17 11:02
Mathlib/RingTheory/Norm/Basic.lean
feat: add `Algebra.norm_zpow` (#40238) …
Modified Algebra.norm_invView on Github →
2026-01-05 14:32
Mathlib/RingTheory/Norm/Basic.lean
feat(RepresentationTheory/Homological/GroupCohomology/Hilbert90): add Hilbert 90 for cyclic groups (#33124) …
Added Algebra.norm_invView on Github →