Theorems · Inductive type · ring theory
WithConv
Sort u_1 → Sort (max 1 u_1)
A type synonym for the convolutive product of linear maps and intrinsic star.
The instances for the convolutive product and intrinsic star are only available with this type.
Use WithConv.linearEquiv to coerce into this type.
- Defined in
- Mathlib.Algebra.WithConv
- Cited by
- 138 results in Mathlib
- Foundations
- Depth 0 from the axioms, rests on 1 definitions · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites0
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Nothing in Mathlib beyond the foundations.
Cited by158
Results whose statement or proof uses this declaration.
- WithConv.ofConvstatement and proof · cited by 97
- WithConv.extstatement and proof · cited by 25
- WithConv.addEquivstatement and proof · cited by 10
- WithConv.toConv_injectivestatement · cited by 6
- WithConv.congrstatement · cited by 4
- WithConv.congrLinearEquivstatement · cited by 4
- WithConv.linearEquivstatement and proof · cited by 4
- WithConv.ofConv_injectivestatement · cited by 4
- WithConv.equivstatement · cited by 3
- Coalgebra.Repr.convMul_applystatement and proof · cited by 3
- LinearMap.toMatrix'_intrinsicStarstatement and proof · cited by 2
- TensorProduct.intrinsicStar_mapstatement and proof · cited by 2