Theorem JacobsonNoether.exists_pow_mem_center_of_inseparable

Modification history

2024-11-22 13:03
Mathlib/FieldTheory/JacobsonNoether.lean
feat(FieldTheory.JacobsonNoether) : add proof of the Jacobson-Noether theorem (#16525) …
Added JacobsonNoether.exists_pow_mem_center_of_inseparableView on Github →