Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-12-08 17:29 8cfcef09

View on Github →

feat(algebra/linear_algebra): add product construction for modules

Estimated changes

Created algebra/linear_algebra/prod_module.lean

added theorem prod.fst_inl

added theorem prod.fst_inr

added theorem prod.fst_inv

added theorem prod.fst_mul

added theorem prod.fst_one

added theorem prod.fst_prod

added theorem prod.injective_inl

added theorem prod.injective_inr

added def prod.inl

added theorem prod.inl_eq_inl

added theorem prod.inl_eq_inr

added def prod.inr

added theorem prod.inr_eq_inl

added theorem prod.inr_eq_inr

added theorem prod.is_basis_inl_union_inr

added theorem prod.is_linear_map_prod_fst

added theorem prod.is_linear_map_prod_inl

added theorem prod.is_linear_map_prod_inr

added theorem prod.is_linear_map_prod_mk

added theorem prod.is_linear_map_prod_snd

added theorem prod.linear_independent_inl_union_inr

added theorem prod.snd_inl

added theorem prod.snd_inr

added theorem prod.snd_inv

added theorem prod.snd_mul

added theorem prod.snd_one

added theorem prod.snd_prod

added theorem prod.span_inl_union_inr

added theorem prod.span_prod