Commit 2020-10-12 14:57 3d1f16aa

View on Github →

feat(analysis/normed_space/multilinear): define mk_pi_algebra (#4316) I'm going to use this definition for converting (mv_)power_series to formal_multilinear_series.

Estimated changes

Modified src/analysis/normed_space/multilinear.lean

added theorem continuous_multilinear_map.mk_pi_algebra_apply

added theorem continuous_multilinear_map.mk_pi_algebra_fin_apply

added theorem continuous_multilinear_map.mk_pi_field_apply_one_eq_self

deleted theorem continuous_multilinear_map.mk_pi_ring_apply_one_eq_self

added theorem continuous_multilinear_map.norm_mk_pi_algebra

added theorem continuous_multilinear_map.norm_mk_pi_algebra_fin

added theorem continuous_multilinear_map.norm_mk_pi_algebra_fin_le_of_pos

added theorem continuous_multilinear_map.norm_mk_pi_algebra_fin_succ_le

added theorem continuous_multilinear_map.norm_mk_pi_algebra_fin_zero

added theorem continuous_multilinear_map.norm_mk_pi_algebra_le

added theorem continuous_multilinear_map.norm_mk_pi_algebra_of_empty

Modified src/linear_algebra/multilinear.lean

added theorem linear_map.coe_comp_multilinear_map

modified def linear_map.comp_multilinear_map

added theorem linear_map.comp_multilinear_map_apply

added theorem multilinear_map.mk_pi_algebra_apply

added theorem multilinear_map.mk_pi_algebra_fin_apply

added theorem multilinear_map.mk_pi_algebra_fin_apply_const

added def multilinear_map.smul_right

added theorem multilinear_map.smul_right_apply

Modified src/topology/algebra/multilinear.lean

added theorem continuous_multilinear_map.to_multilinear_map_inj