Commit 2023-02-28 09:43 cd441518

View on Github →

feat: Port Algebra.Module.Submodule.Bilinear (#2531)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Module/Submodule/Bilinear.lean

added theorem Submodule.apply_mem_map₂

added theorem Submodule.image2_subset_map₂

added def Submodule.map₂

added theorem Submodule.map₂_bot_left

added theorem Submodule.map₂_bot_right

added theorem Submodule.map₂_eq_span_image2

added theorem Submodule.map₂_flip

added theorem Submodule.map₂_le

added theorem Submodule.map₂_le_map₂

added theorem Submodule.map₂_le_map₂_left

added theorem Submodule.map₂_le_map₂_right

added theorem Submodule.map₂_span_singleton_eq_map

added theorem Submodule.map₂_span_singleton_eq_map_flip

added theorem Submodule.map₂_span_span

added theorem Submodule.map₂_sup_left

added theorem Submodule.map₂_sup_right

added theorem Submodule.map₂_supᵢ_left

added theorem Submodule.map₂_supᵢ_right