Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-06-09 06:11 faa58e51

View on Github →

refactor(algebra/module/projective) make is_projective a class (#7830) Make is_projective a class.

Estimated changes

Modified src/algebra/category/Module/projective.lean

Modified src/algebra/module/projective.lean

deleted theorem is_projective.lifting_property

deleted theorem is_projective.of_free

deleted theorem is_projective.of_lifting_property'

deleted theorem is_projective.of_lifting_property

deleted def is_projective

added theorem module.projective_def

added theorem module.projective_lifting_property

added theorem module.projective_of_free

added theorem module.projective_of_lifting_property'

added theorem module.projective_of_lifting_property