Commit 2023-04-10 15:18 6ab1bde3

View on Github →

feat: port Algebra.Module.Projective (#3335)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Module/Projective.lean

added theorem Module.Projective.of_basis

added theorem Module.Projective.of_lifting_property''

added theorem Module.Projective.of_lifting_property'

added theorem Module.Projective.of_lifting_property

added theorem Module.projective_def'

added theorem Module.projective_def

added theorem Module.projective_lifting_property

Modified Mathlib/Algebra/Star/Module.lean

added theorem IsSelfAdjoint.coe_selfAdjointPart_apply

added theorem IsSelfAdjoint.selfAdjointPart_apply

added theorem IsSelfAdjoint.skewAdjointPart_apply

modified def selfAdjointPart

added theorem selfAdjointPart_comp_subtype_selfAdjoint

added theorem selfAdjointPart_comp_subtype_skewAdjoint

modified def skewAdjointPart

added theorem skewAdjointPart_comp_subtype_selfAdjoint

added theorem skewAdjointPart_comp_subtype_skewAdjoint

Modified Mathlib/LinearAlgebra/Dfinsupp.lean

added theorem Dfinsupp.coprodMap_apply_single

Modified Mathlib/LinearAlgebra/Finsupp.lean

added theorem Finsupp.apply_total_id

Modified Mathlib/LinearAlgebra/Prod.lean

added theorem LinearMap.coprod_zero_left

added theorem LinearMap.coprod_zero_right

modified theorem LinearMap.fst_prod

modified theorem LinearMap.pair_fst_snd

modified def LinearMap.prod

added theorem LinearMap.prod_comp

modified theorem LinearMap.snd_prod

Modified Mathlib/LinearAlgebra/Projection.lean