Mathlib Changelog
v4
Changelog
About
Github
Theorem
galRestrict'_id
Modification history
2025-09-03 14:38
Mathlib/RingTheory/IntegralClosure/IntegralRestrict.lean
feat(Ideal): `relNorm` is preserved under the action of an `AlgEquiv` (#28724) …
Added
galRestrict'_id
View on Github →