Structures · Algebra
Algebra.SubmersivePresentation.HasCoeffs
A type class witnessing the fact that R₀ contains enough coefficients to descend
P to a submersive presentation.
- Shape
- 2 explicit arguments · adds coeffs_subset_range
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 by15
- Algebra.SubmersivePresentation.jacobianOfHasCoeffs
- Algebra.SubmersivePresentation.invJacobianOfHasCoeffs
- Algebra.SubmersivePresentation.jacobianRelationsOfHasCoeffs
- Algebra.SubmersivePresentation.map_invJacobianOfHasCoeffs
- Algebra.SubmersivePresentation.map_jacobianOfHasCoeffs
- Algebra.SubmersivePresentation.HasCoeffs.coeffs_subset_range
- Algebra.SubmersivePresentation.map_jacobianRelationsOfHasCoeffs
- Algebra.SubmersivePresentation.ofHasCoeffs
- Algebra.SubmersivePresentation.jacobianRelationsOfHasCoeffs.congr_simp
- Algebra.SubmersivePresentation.aeval_jacobianOfHasCoeffs
- Algebra.SubmersivePresentation.invJacobianOfHasCoeffs.congr_simp
- Algebra.SubmersivePresentation.aeval_invJacobianOfHasCoeffs
- Algebra.SubmersivePresentation.sum_jacobianRelationsOfHasCoeffs_mul_relationOfHasCoeffs
- Algebra.SubmersivePresentation.jacobianOfHasCoeffs.congr_simp
- Algebra.SubmersivePresentation.instHasCoeffs
Ancestors0
No ancestors.