Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2018-09-20 19:21
9aec1d18
View on Github →
refactor(algebra/pi_instances): move prod instances to pi_instances file
Estimated changes
Modified
algebra/group.lean
Modified
algebra/pi_instances.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.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
Modified
linear_algebra/prod_module.lean
added
theorem
is_basis_inl_union_inr
added
theorem
is_linear_map_prod_fst
added
theorem
is_linear_map_prod_inl
added
theorem
is_linear_map_prod_inr
added
theorem
is_linear_map_prod_mk
added
theorem
is_linear_map_prod_snd
added
theorem
linear_independent_inl_union_inr
deleted
theorem
prod.fst_inl
deleted
theorem
prod.fst_inr
deleted
theorem
prod.fst_inv
deleted
theorem
prod.fst_mul
deleted
theorem
prod.fst_one
deleted
theorem
prod.fst_prod
deleted
theorem
prod.injective_inl
deleted
theorem
prod.injective_inr
deleted
def
prod.inl
deleted
theorem
prod.inl_eq_inl
deleted
theorem
prod.inl_eq_inr
deleted
def
prod.inr
deleted
theorem
prod.inr_eq_inl
deleted
theorem
prod.inr_eq_inr
deleted
theorem
prod.is_basis_inl_union_inr
deleted
theorem
prod.is_linear_map_prod_fst
deleted
theorem
prod.is_linear_map_prod_inl
deleted
theorem
prod.is_linear_map_prod_inr
deleted
theorem
prod.is_linear_map_prod_mk
deleted
theorem
prod.is_linear_map_prod_snd
deleted
theorem
prod.linear_independent_inl_union_inr
deleted
theorem
prod.snd_inl
deleted
theorem
prod.snd_inr
deleted
theorem
prod.snd_inv
deleted
theorem
prod.snd_mul
deleted
theorem
prod.snd_one
deleted
theorem
prod.snd_prod
deleted
theorem
prod.span_inl_union_inr
deleted
theorem
prod.span_prod
added
theorem
span_inl_union_inr
added
theorem
span_prod