Structures · Algebra
LinearMap.IsPerfPair
For a ring R and two modules M and N, a perfect pairing is a bilinear map M × N → R
that is bijective in both arguments.
- Shape
- One type argument · adds bijective_left, bijective_right
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by29
- LinearMap.toPerfPair
- Module.IsReflexive.of_isPerfPair
- LinearMap.toPerfPair.congr_simp
- LinearMap.apply_symm_toPerfPair_self
- LinearMap.IsPerfectCompl.isCompl_right
- LinearMap.IsPerfectCompl.flip
- RootPairing.mk''
- LinearMap.IsPerfectCompl.left_top_iff
- RootPairing.mk.congr_simp
- LinearMap.IsPerfectCompl.congr_simp
- LinearMap.IsPerfPair.bijective_left
- LinearMap.exists_basis_basis_of_span_eq_top_of_mem_algebraMap
- LinearMap.IsPerfectCompl.isCompl_left
- LinearMap.IsPerfPair.restrict
- LinearMap.finrank_eq_of_isPerfPair
- LinearMap.IsPerfPair.bijective_right
- LinearMap.apply_toPerfPair_flip
- LinearMap.IsPerfectCompl.flip_iff
- Module.finrank_of_isPerfPair
- LinearMap.IsPerfPair.restrictScalars_of_field
- LinearMap.IsPerfPair.restrictScalars
- RootPairing.mk'
- LinearMap.flip.instIsPerfPair
- LinearMap.IsPerfPair.congr
- RootPairing.isRootSystem_mk''
- LinearMap.toLinearMap_toPerfPair
- LinearMap.IsPerfectCompl.right_top_iff
- LinearMap.IsPerfPair.compl₁₂
- LinearMap.toPerfPair_apply
Ancestors0
No ancestors.