Theorem galRestrict_symm_algebraMap_apply

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_symm_algebraMap_applyView on Github →