Commit 2022-12-07 02:18 6fad74b7

View on Github →

chore: fix SMulZeroClass and DistribSMul names (#894) No other branches seem to be affected by this change, afaict.

Estimated changes

Modified Mathlib/GroupTheory/GroupAction/Defs.lean

added def Function.Surjective.distribSMulLeft

deleted def Function.Surjective.distribSmulLeft

modified def Function.Surjective.smulZeroClassLeft

added def SMulZeroClass.compFun

added def SMulZeroClass.toZeroHom

deleted def SmulZeroClass.compFun

deleted def SmulZeroClass.toZeroHom

Modified Mathlib/GroupTheory/GroupAction/Units.lean