def
bilin_form.tensor_distrib'
{R : Type u_2}
{A : Type u_3}
{M₁ : Type u_4}
{M₂ : Type u_5}
[comm_semiring R]
[comm_semiring A]
[add_comm_monoid M₁]
[add_comm_monoid M₂]
[algebra R A]
[module R M₁]
[module A M₁]
[smul_comm_class R A M₁]
[smul_comm_class A R M₁]
[smul_comm_class R A A]
[is_scalar_tower R A M₁]
[module R M₂] :
tensor_product R (bilin_form A M₁) (bilin_form R M₂) →ₗ[A] bilin_form A (tensor_product R M₁ M₂)
The tensor product of two bilinear forms injects into bilinear forms on tensor products.
Equations
- bilin_form.tensor_distrib' = (((tensor_product.algebra_tensor_module.tensor_tensor_tensor_comm R A M₁ M₂ M₁ M₂).dual_map.trans (tensor_product.lift.equiv A (tensor_product R M₁ M₂) (tensor_product R M₁ M₂) A).symm).trans linear_map.to_bilin).to_linear_map.comp ((tensor_product.algebra_tensor_module.dual_distrib R A (tensor_product A M₁ M₁) (tensor_product R M₂ M₂)).comp (tensor_product.algebra_tensor_module.congr (bilin_form.to_lin.trans (tensor_product.lift.equiv A M₁ M₁ A)) (bilin_form.to_lin.trans (tensor_product.lift.equiv R M₂ M₂ R))).to_linear_map)
@[simp]
theorem
bilin_form.tensor_distrib'_tmul
{R : Type u_2}
{A : Type u_3}
{M₁ : Type u_4}
{M₂ : Type u_5}
[comm_semiring R]
[comm_semiring A]
[add_comm_monoid M₁]
[add_comm_monoid M₂]
[algebra R A]
[module R M₁]
[module A M₁]
[smul_comm_class R A M₁]
[smul_comm_class A R M₁]
[smul_comm_class R A A]
[is_scalar_tower R A M₁]
[module R M₂]
(B₁ : bilin_form A M₁)
(B₂ : bilin_form R M₂)
(m₁ : M₁)
(m₂ : M₂)
(m₁' : M₁)
(m₂' : M₂) :
@[protected, reducible]
def
bilin_form.tmul'
{R : Type u_2}
{A : Type u_3}
{M₁ : Type u_4}
{M₂ : Type u_5}
[comm_semiring R]
[comm_semiring A]
[add_comm_monoid M₁]
[add_comm_monoid M₂]
[algebra R A]
[module R M₁]
[module A M₁]
[smul_comm_class R A M₁]
[smul_comm_class A R M₁]
[smul_comm_class R A A]
[is_scalar_tower R A M₁]
[module R M₂]
(B₁ : bilin_form A M₁)
(B₂ : bilin_form R M₂) :
bilin_form A (tensor_product R M₁ M₂)
The tensor product of two bilinear forms, a shorthand for dot notation.
theorem
bilin_form.is_symm.tmul
{R : Type u_2}
{M₁ : Type u_4}
{M₂ : Type u_5}
[comm_semiring R]
[add_comm_monoid M₁]
[add_comm_monoid M₂]
[module R M₁]
[module R M₂]
{B₁ : bilin_form R M₁}
{B₂ : bilin_form R M₂}
(hB₁ : B₁.is_symm)
(hB₂ : B₂.is_symm) :
theorem
quadratic_form.pos_def.tmul
{M₁ : Type u_4}
{M₂ : Type u_5}
[add_comm_group M₁]
[add_comm_group M₂]
[module ℝ M₁]
[module ℝ M₂]
{B₁ : bilin_form ℝ M₁}
{B₂ : bilin_form ℝ M₂}
(hB₁ : B₁.to_quadratic_form.pos_def)
(hB₂ : B₂.to_quadratic_form.pos_def) :
(B₁.tmul B₂).to_quadratic_form.pos_def
Note: this declaration is incomplete and uses sorry.