Commit 2024-11-22 13:03 d380d2c9

View on Github →

feat(FieldTheory.JacobsonNoether) : add proof of the Jacobson-Noether theorem (#16525) In this PR we provide a proof of the Jacobson-Noether theorem following this blog Co-authored by: Filippo A. E. Nuccio @faenuccio Co-authored by: Wanyi He @Blackfeather007 Co-authored by: Huanyu Zheng @Yu-Misaka Co-authored by: Yi Yuan @yuanyi-350 Co-authored by: Weichen Jiao @AlbertJ-314 Co-authored by: Sihan Wu @Old-Turtledove Co-authored by: @FR-vdash-bot

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Algebra/Basic.lean

Created Mathlib/Algebra/CharP/LinearMaps.lean

added theorem Module.charP_end

Modified Mathlib/Algebra/CharP/Subring.lean

added theorem CharP.charP_center_iff

added theorem ExpChar.expChar_center_iff

Modified Mathlib/Algebra/GroupWithZero/Conj.lean

added theorem GroupWithZero.conj_pow₀

added theorem GroupWithZero.isConj_iff₀

deleted theorem isConj_iff₀

Created Mathlib/FieldTheory/JacobsonNoether.lean

added theorem JacobsonNoether.exist_pow_eq_zero_of_le

added theorem JacobsonNoether.exists_pow_mem_center_of_inseparable'

added theorem JacobsonNoether.exists_pow_mem_center_of_inseparable

added theorem JacobsonNoether.exists_separable_and_not_isCentral'

added theorem JacobsonNoether.exists_separable_and_not_isCentral