Theorem Algebra.IsQuadraticExtension.isMulCommutative_galoisGroup

Modification history

2026-10-16 07:34
Mathlib/FieldTheory/Galois/Basic.lean
chore: remove declarations deprecated between 2026-04-01 and 2026-04-15 (#44903) …
Deleted Algebra.IsQuadraticExtension.isMulCommutative_galoisGroupView on Github →
2026-04-09 05:37
Mathlib/FieldTheory/Galois/Basic.lean
fix(FieldTheory/Galois/Basic): `inferInstance` instance should be a theorem (#37822) …
Added Algebra.IsQuadraticExtension.isMulCommutative_galoisGroupView on Github →