Theorem IsGaloisGroup.smulCommClassQuotient

Modification history

2026-08-04 14:58

Mathlib/RingTheory/IsGaloisGroup/Basic.lean

chore(RingTheory/IsGaloisGroup/Basic): automated extraction from #42430 (#42433) …

Added IsGaloisGroup.smulCommClassQuotient View on Github →