Theorems · Definition · linear algebra
LinearMap.BilinForm
(R : Type u_2) → [inst : CommSemiring R] → (M : Type u_5) → [inst_1 : AddCommMonoid M] → [Module R M] → Type (max u_2 u_5)
For convenience, a shorthand for the type of bilinear forms from M to R.
- Defined in
- Mathlib.LinearAlgebra.BilinearMap
- Cited by
- 501 results in Mathlib
- Foundations
- Depth 33 from the axioms, rests on 327 definitions · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
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
- AddCommMonoidstatement and proof · cited by 12,281
- CommSemiringstatement and proof · cited by 10,911
- LinearMap.BilinMapproof · cited by 85
Cited by607
Results whose statement or proof uses this declaration.
- LinearMap.BilinForm.Nondegeneratestatement and proof · cited by 77
- LinearMap.BilinForm.toMatrixstatement · cited by 47
- LieModule.traceFormstatement · cited by 41
- RootPairing.RootFormstatement · cited by 41
- LinearMap.BilinForm.orthogonalstatement and proof · cited by 36
- LinearMap.BilinForm.IsSymmstatement · cited by 35
- killingFormstatement · cited by 34
- Algebra.traceFormstatement · cited by 33
- RootPairing.InvariantForm.formstatement · cited by 33
- LinearMap.BilinForm.IsReflstatement and proof · cited by 30
- LinearMap.BilinForm.restrictstatement and proof · cited by 24
- LinearMap.BilinForm.extstatement and proof · cited by 22
Showing the 200 most cited of 607.