Commit 2024-04-22 08:47 7877b40e

View on Github →

feat(Ring/InjSurj): add missing lemmas (#12328) Add Function.(Inj|Surj)ective.(left|right)DistribClass.

Estimated changes

Modified Mathlib/Algebra/Ring/InjSurj.lean

added theorem Function.Injective.leftDistribClass

added theorem Function.Injective.rightDistribClass

added theorem Function.Surjective.leftDistribClass

added theorem Function.Surjective.rightDistribClass