Theorems · Definition · ring theory
LinearMap.mul
(R : Type u_1) →
(A : Type u_2) →
[inst : CommSemiring R] →
[inst_1 : NonUnitalNonAssocSemiring A] →
[inst_2 : Module R A] → [SMulCommClass R A A] → [IsScalarTower R A A] → A →ₗ[R] A →ₗ[R] AThe multiplication in a non-unital non-associative algebra is a bilinear map.
A weaker version of this for semirings exists as AddMonoidHom.mul.
- Defined in
- Mathlib.Algebra.Algebra.Bilinear
- Cited by
- 61 results in Mathlib
- Foundations
- Depth 36 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Modulestatement and proof · cited by 20,661
- RingHom.idstatement · cited by 18,349
- CommSemiringstatement and proof · cited by 10,911
- LinearMapstatement · cited by 10,215
- IsScalarTowerstatement and proof · cited by 3,896
- SMulCommClassstatement and proof · cited by 1,927
- NonUnitalNonAssocSemiringstatement and proof · cited by 1,081
- LinearMap.mk₂proof · cited by 5
Cited by82
Results whose statement or proof uses this declaration.
- ContinuousLinearMap.mulproof · cited by 63
- LinearMap.mul'proof · cited by 47
- Algebra.TensorProduct.liftproof · cited by 46
- Submodule.mulMapproof · cited by 43
- LieModule.traceFormproof · cited by 41
- LinearMap.mul_apply_applystatement and proof · cited by 25
- Submodule.span_mul_spanproof · cited by 18
- Polynomial.wronskianBilinproof · cited by 8
- PiTensorProduct.mulproof · cited by 8
- LinearMap.BilinForm.baseChangeproof · cited by 7
- Submodule.mul_eq_map₂statement and proof · cited by 6
- Algebra.norm_selfproof · cited by 6