Commit 2026-10-17 10:55 0f906b6f
View on Github →feat(Algebra/Field/Subfield): Subfield.isMulCommutative_closure (#44921)
Prove that the subfield closure of commuting elements is commutative. Also rename the motive argument of Subfield.closure_induction to motive.