mathlib3 documentation

lean-ga / for_mathlib.linear_algebra.bilinear_form.basic

source
@[protected, instance]
def bilin_form.smul_comm_class {α : Type u_1} {β : Type u_2} {R : Type u_3} {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] [monoid α] [monoid β] [distrib_mul_action α R] [distrib_mul_action β R] [smul_comm_class α R R] [smul_comm_class β R R] [smul_comm_class α β R] :
smul_comm_class α β (bilin_form R M)
source
@[protected, instance]
def bilin_form.is_scalar_tower {α : Type u_1} {β : Type u_2} {R : Type u_3} {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] [monoid α] [monoid β] [distrib_mul_action α R] [distrib_mul_action β R] [smul_comm_class α R R] [smul_comm_class β R R] [has_smul α β] [is_scalar_tower α β R] :
is_scalar_tower α β (bilin_form R M)
source
@[simp]
theorem bilin_form.linear_map.to_bilin_apply {R : Type u_3} {M : Type u_4} [comm_semiring R] [add_comm_monoid M] [module R M] (l : M →ₗ[R] M →ₗ[R] R) (v w : M) :
⇑(⇑linear_map.to_bilin l) v w = ⇑(⇑l v) w