Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-05 22:44 9d3c709d

View on Github →

chore(algebra/module): Reuse proofs from subgroup (#3631) Confusingly these have opposite names - someone can always fix the names later though.

Estimated changes