Structures · Algebra
Module.Oriented
A type class fixing an orientation of a module.
- Defined in
- Mathlib.LinearAlgebra.Orientation
- Shape
- 3 explicit arguments · adds positiveOrientation
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 by191
- EuclideanGeometry.oangle
- EuclideanGeometry.o
- EuclideanGeometry.oangle_rotate_sign
- EuclideanGeometry.oangle_eq_angle_of_sign_eq_one
- Module.Oriented.positiveOrientation
- EuclideanGeometry.angle_eq_pi_div_two_of_oangle_eq_pi_div_two
- EuclideanGeometry.angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two
- EuclideanGeometry.left_ne_of_oangle_eq_pi_div_two
- EuclideanGeometry.oangle.congr_simp
- EuclideanGeometry.oangle_rev
- EuclideanGeometry.oangle_self_right
- Sbtw.oangle_eq_right
- EuclideanGeometry.oangle_eq_of_dist_orthogonalProjection_eq
- EuclideanGeometry.oangle_self_left
- Sbtw.oangle_eq_left
- EuclideanGeometry.right_ne_of_oangle_eq_pi_div_two
- EuclideanGeometry.oangle_pointReflection_right
- EuclideanGeometry.right_ne_of_oangle_ne_zero
- EuclideanGeometry.oangle_add
- EuclideanGeometry.left_ne_right_of_oangle_ne_zero
- EuclideanGeometry.left_ne_of_oangle_ne_zero
- EuclideanGeometry.oangle_ne_zero_and_ne_pi_iff_affineIndependent
- Affine.Triangle.eq_excenter_of_two_zsmul_oangle_eq
- EuclideanGeometry.oangle_eq_zero_or_eq_pi_iff_collinear
- EuclideanGeometry.angle_eq_abs_oangle_toReal
- Sbtw.oangle_eq_add_pi_left
- EuclideanGeometry.oangle_swap₁₃_sign
- Sbtw.oangle₁₂₃_eq_pi
- Collinear.two_zsmul_oangle_eq_left
- EuclideanGeometry.collinear_iff_of_two_zsmul_oangle_eq
- Wbtw.oangle_eq_left
- Wbtw.oangle₃₁₂_eq_zero
- Wbtw.oangle₂₁₃_eq_zero
- EuclideanGeometry.oangle_eq_zero_iff_angle_eq_zero
- Affine.Triangle.dist_orthogonalProjectionSpan_faceOpposite_eq_iff_two_zsmul_oangle_eq
- EuclideanGeometry.Sphere.dist_div_sin_oangle_div_two_eq_radius
- EuclideanGeometry.abs_oangle_right_toReal_lt_pi_div_two_of_dist_eq
- EuclideanGeometry.dist_orthogonalProjection_eq_of_oangle_eq
- Sbtw.oangle_sign_eq
- Collinear.oangle_sign_of_sameRay_vsub
- EuclideanGeometry.Sphere.dist_div_cos_oangle_center_div_two_eq_radius
- EuclideanGeometry.oangle_midpoint_rev_left
- EuclideanGeometry.cospherical_of_two_zsmul_oangle_eq_of_not_collinear
- EuclideanGeometry.oangle_swap₁₂_sign
- EuclideanGeometry.oangle_eq_angle_or_eq_neg_angle
- Affine.Triangle.circumsphere_eq_circumsphere_of_eq_of_eq_of_two_zsmul_oangle_eq
- EuclideanGeometry.Sphere.tan_div_two_smul_rotation_pi_div_two_vadd_midpoint_eq_center
- Wbtw.oangle_sign_eq_of_ne_left
- EuclideanGeometry.abs_oangle_toReal_lt_pi_div_two_of_angle_eq_pi_div_two
- Collinear.two_zsmul_oangle_eq_right
Ancestors0
No ancestors.