Theorem Subfield.isMulCommutative_closure

Modification history

2026-10-17 10:55
Mathlib/Algebra/Field/Subfield/Basic.lean
feat(Algebra/Field/Subfield): `Subfield.isMulCommutative_closure` (#44921) …
Added Subfield.isMulCommutative_closureView on Github →