Theorem Algebra.map_intNormAux

Modification history

2024-08-07 14:38

Mathlib/RingTheory/IntegralClosure/IntegralRestrict.lean

chore: backports for leanprover/lean4#4814 (part 29) (#15572)

Modified Algebra.map_intNormAux View on Github →

2024-07-04 13:06

Mathlib/RingTheory/IntegralRestrict.lean

feat(FieldTheory/Separable): add elementwise `IsSeparable` and rename the old to `Algebra.IsSeparable` (#14232) …

Modified Algebra.map_intNormAux View on Github →

2024-01-09 09:24

Mathlib/RingTheory/IntegralRestrict.lean

feat: Define `intNorm` and `intTrace`. (#9265)

Added Algebra.map_intNormAux View on Github →