Skip to content

feat(RingTheory): generalize relNorm_eq_pow_of_isMaximal to separable fraction field extensions - #41696

Open
vaca22 wants to merge 4 commits into
leanprover-community:masterfrom
vaca22:generalize-relnorm-separable
Open

feat(RingTheory): generalize relNorm_eq_pow_of_isMaximal to separable fraction field extensions#41696
vaca22 wants to merge 4 commits into
leanprover-community:masterfrom
vaca22:generalize-relnorm-separable

feat(FieldTheory/Galois): the normal closure of a separable extension…

6c04cca
Select commit
Loading
Failed to load commit list.
Sign in for the full log view

Annotations

1 warning
Lint and suggest
succeeded Jul 27, 2026 in 2m 7s