Rotation

📁 Source: Mathlib/Geometry/Euclidean/Angle/Oriented/Rotation.lean

Statistics

Metric	Count
Definitions rotation, rotationAux	2
Theorems rotation, det_rotation, eq_rotation_self_iff, eq_rotation_self_iff_angle_eq_zero, exists_linearIsometryEquiv_eq_of_det_pos, inner_eq_zero_iff_eq_zero_or_eq_smul_rotation_pi_div_two, inner_rotation_pi_div_two_left, inner_rotation_pi_div_two_left_smul, inner_rotation_pi_div_two_right, inner_rotation_pi_div_two_right_smul, inner_smul_rotation_pi_div_two_left, inner_smul_rotation_pi_div_two_right, inner_smul_rotation_pi_div_two_smul_left, inner_smul_rotation_pi_div_two_smul_right, kahler_rotation_left, kahler_rotation_left', kahler_rotation_right, linearEquiv_det_rotation, neg_rotation, neg_rotation_neg_pi_div_two, neg_rotation_pi_div_two, oangle_eq_iff_eq_norm_div_norm_smul_rotation_of_ne_zero, oangle_eq_iff_eq_norm_div_norm_smul_rotation_or_eq_zero, oangle_eq_iff_eq_pos_smul_rotation_of_ne_zero, oangle_eq_iff_eq_pos_smul_rotation_or_eq_zero, oangle_rotation, oangle_rotation_left, oangle_rotation_oangle_left, oangle_rotation_oangle_right, oangle_rotation_right, oangle_rotation_self_left, oangle_rotation_self_right, rotationAux_apply, rotation_apply, rotation_eq_matrix_toLin, rotation_eq_self_iff, rotation_eq_self_iff_angle_eq_zero, rotation_map, rotation_map_complex, rotation_neg_orientation_eq_neg, rotation_oangle_eq_iff_norm_eq, rotation_pi, rotation_pi_apply, rotation_pi_div_two, rotation_rotation, rotation_symm, rotation_symm_apply, rotation_trans, rotation_zero	49
Total	51

Complex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
rotation 📖	mathematical	—	DFunLike.coe LinearIsometryEquiv Real Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Complex NormedAddCommGroup.toSeminormedAddCommGroup instNormedAddCommGroup NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike instInnerProductSpaceRealComplex EquivLike.toFunLike LinearIsometryEquiv.instEquivLike Orientation.rotation finrank_real_complex_fact orientation instMul Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Ring.toSemiring SeminormedRing.toRing SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField SetLike.instMembership Submonoid.instSetLike Submonoid.unitSphere Real.Angle.toCircle	—	RingHomInvPair.ids finrank_real_complex_fact rightAngleRotation Real.Angle.coe_toCircle Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add

Orientation

Definitions

Name	Category	Theorems
rotation 📖	CompOp	59 math math: inner_rotation_pi_div_two_right_smul, oangle_add_left_smul_rotation_pi_div_two, linearEquiv_det_rotation, tan_oangle_add_left_smul_rotation_pi_div_two, rotation_eq_self_iff, neg_rotation, eq_rotation_self_iff_angle_eq_zero, tan_oangle_add_right_smul_rotation_pi_div_two, EuclideanGeometry.dist_eq_iff_eq_smul_rotation_pi_div_two_vadd_midpoint, neg_rotation_neg_pi_div_two, det_rotation, rotation_pi_apply, rotation_rotation, rotation_map_complex, rotation_symm, rotation_map, oangle_rotation_left, EuclideanGeometry.Sphere.tan_div_two_smul_rotation_pi_div_two_vadd_midpoint_eq_center, exists_linearIsometryEquiv_eq_of_det_pos, oangle_rotation_oangle_right, inner_rotation_pi_div_two_right, oangle_rotation, inner_rotation_pi_div_two_left, oangle_rotation_self_left, Affine.Triangle.circumsphere_eq_of_dist_of_oangle, oangle_eq_iff_eq_pos_smul_rotation_of_ne_zero, inner_rotation_pi_div_two_left_smul, rotation_neg_orientation_eq_neg, eq_rotation_self_iff, oangle_eq_iff_eq_pos_smul_rotation_or_eq_zero, rotation_zero, oangle_rotation_oangle_left, EuclideanGeometry.Sphere.inv_tan_div_two_smul_rotation_pi_div_two_vadd_midpoint_eq_center, rotation_eq_self_iff_angle_eq_zero, Affine.Triangle.inv_tan_div_two_smul_rotation_pi_div_two_vadd_midpoint_eq_circumcenter, oangle_rotation_right, rotation_trans, oangle_sub_right_smul_rotation_pi_div_two, inner_smul_rotation_pi_div_two_right, kahler_rotation_left', neg_rotation_pi_div_two, rotation_eq_matrix_toLin, oangle_sub_left_smul_rotation_pi_div_two, oangle_eq_iff_eq_norm_div_norm_smul_rotation_or_eq_zero, oangle_add_right_smul_rotation_pi_div_two, inner_smul_rotation_pi_div_two_left, kahler_rotation_left, inner_eq_zero_iff_eq_zero_or_eq_smul_rotation_pi_div_two, oangle_eq_iff_eq_norm_div_norm_smul_rotation_of_ne_zero, rotation_apply, kahler_rotation_right, rotation_pi_div_two, oangle_rotation_self_right, inner_smul_rotation_pi_div_two_smul_left, inner_smul_rotation_pi_div_two_smul_right, rotation_pi, rotation_symm_apply, rotation_oangle_eq_iff_norm_eq, Complex.rotation
rotationAux 📖	CompOp	1 math math: rotationAux_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
det_rotation 📖	mathematical	—	DFunLike.coe MonoidHom LinearMap Real CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring MonoidHom.instFunLike LinearMap.det LinearEquiv.toLinearMap Real.semiring RingHomInvPair.ids LinearIsometryEquiv.toLinearEquiv rotation Real.instOne	—	Real.instIsStrictOrderedRing RingHomInvPair.ids exists_ne Module.nontrivial_of_finrank_eq_succ Real.instNontrivial Fact.out smulCommClass_self Finite.of_fintype rotation_eq_matrix_toLin LinearMap.det_toLin Matrix.det_fin_two_of neg_mul sub_neg_eq_add sq Real.Angle.cos_sq_add_sin_sq
eq_rotation_self_iff 📖	mathematical	—	DFunLike.coe LinearIsometryEquiv Real Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike EquivLike.toFunLike LinearIsometryEquiv.instEquivLike rotation NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Real.Angle Real.instNormedAddCommGroupAngle	—	Real.instIsStrictOrderedRing RingHomInvPair.ids rotation_eq_self_iff
eq_rotation_self_iff_angle_eq_zero 📖	mathematical	—	DFunLike.coe LinearIsometryEquiv Real Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike EquivLike.toFunLike LinearIsometryEquiv.instEquivLike rotation Real.Angle NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Real.instNormedAddCommGroupAngle	—	Real.instIsStrictOrderedRing RingHomInvPair.ids rotation_eq_self_iff_angle_eq_zero
exists_linearIsometryEquiv_eq_of_det_pos 📖	mathematical	Real Real.instLT Real.instZero DFunLike.coe MonoidHom LinearMap CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring MonoidHom.instFunLike LinearMap.det LinearEquiv.toLinearMap Real.semiring RingHomInvPair.ids LinearIsometryEquiv.toLinearEquiv	rotation	—	Real.instIsStrictOrderedRing RingHomInvPair.ids exists_ne Module.nontrivial_of_finrank_eq_succ Real.instNontrivial Fact.out LinearIsometryEquiv.toLinearEquiv_injective LinearEquiv.toLinearMap_injective Module.Basis.ext Fintype.complete coe_basisRightAngleRotation LinearIsometryEquiv.norm_map smulCommClass_self linearIsometryEquiv_comp_rightAngleRotation kahler_comp_rightAngleRotation rotation.congr_simp Matrix.cons_val_fin_one
inner_eq_zero_iff_eq_zero_or_eq_smul_rotation_pi_div_two 📖	mathematical	—	Inner.inner Real InnerProductSpace.toInner Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup Real.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace DFunLike.coe LinearIsometryEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids EquivLike.toFunLike LinearIsometryEquiv.instEquivLike rotation Real.Angle.coe DivInvMonoid.toDiv Real.instDivInvMonoid Real.pi instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Real.instIsStrictOrderedRing RingHomInvPair.ids Nat.instAtLeastTwoHAddOfNat inner_zero_left map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass SemilinearIsometryClass.toSemilinearMapClass SemilinearIsometryEquivClass.toSemilinearIsometryClass LinearIsometryEquiv.instSemilinearIsometryEquivClass smul_zero inner_zero_right instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors Real.instIsDomain GroupWithZero.toNoZeroSMulDivisors IsDomain.toIsCancelMulZero EquivLike.toEmbeddingLike eq_zero_or_oangle_eq_iff_inner_eq_zero oangle_eq_iff_eq_pos_smul_rotation_of_ne_zero neg_rotation_pi_div_two smul_neg lt_trichotomy zero_smul IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid neg_neg
inner_rotation_pi_div_two_left 📖	mathematical	—	Inner.inner Real InnerProductSpace.toInner Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup DFunLike.coe LinearIsometryEquiv Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace EquivLike.toFunLike LinearIsometryEquiv.instEquivLike rotation Real.Angle.coe DivInvMonoid.toDiv Real.instDivInvMonoid Real.pi instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.instZero	—	Real.instIsStrictOrderedRing RingHomInvPair.ids Nat.instAtLeastTwoHAddOfNat rotation_pi_div_two inner_rightAngleRotation_self
inner_rotation_pi_div_two_left_smul 📖	mathematical	—	Inner.inner Real InnerProductSpace.toInner Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup DFunLike.coe LinearIsometryEquiv Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace EquivLike.toFunLike LinearIsometryEquiv.instEquivLike rotation Real.Angle.coe DivInvMonoid.toDiv Real.instDivInvMonoid Real.pi instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid Real.instZero	—	Real.instIsStrictOrderedRing RingHomInvPair.ids Nat.instAtLeastTwoHAddOfNat inner_smul_right inner_rotation_pi_div_two_left MulZeroClass.mul_zero
inner_rotation_pi_div_two_right 📖	mathematical	—	Inner.inner Real InnerProductSpace.toInner Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup DFunLike.coe LinearIsometryEquiv Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace EquivLike.toFunLike LinearIsometryEquiv.instEquivLike rotation Real.Angle.coe DivInvMonoid.toDiv Real.instDivInvMonoid Real.pi instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.instZero	—	Real.instIsStrictOrderedRing RingHomInvPair.ids Nat.instAtLeastTwoHAddOfNat real_inner_comm inner_rotation_pi_div_two_left
inner_rotation_pi_div_two_right_smul 📖	mathematical	—	Inner.inner Real InnerProductSpace.toInner Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace DFunLike.coe LinearIsometryEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids EquivLike.toFunLike LinearIsometryEquiv.instEquivLike rotation Real.Angle.coe DivInvMonoid.toDiv Real.instDivInvMonoid Real.pi instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.instZero	—	Real.instIsStrictOrderedRing RingHomInvPair.ids Nat.instAtLeastTwoHAddOfNat real_inner_comm inner_rotation_pi_div_two_left_smul
inner_smul_rotation_pi_div_two_left 📖	mathematical	—	Inner.inner Real InnerProductSpace.toInner Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace DFunLike.coe LinearIsometryEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids EquivLike.toFunLike LinearIsometryEquiv.instEquivLike rotation Real.Angle.coe DivInvMonoid.toDiv Real.instDivInvMonoid Real.pi instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.instZero	—	Real.instIsStrictOrderedRing RingHomInvPair.ids Nat.instAtLeastTwoHAddOfNat inner_smul_left inner_rotation_pi_div_two_left MulZeroClass.mul_zero
inner_smul_rotation_pi_div_two_right 📖	mathematical	—	Inner.inner Real InnerProductSpace.toInner Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace DFunLike.coe LinearIsometryEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids EquivLike.toFunLike LinearIsometryEquiv.instEquivLike rotation Real.Angle.coe DivInvMonoid.toDiv Real.instDivInvMonoid Real.pi instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.instZero	—	Real.instIsStrictOrderedRing RingHomInvPair.ids Nat.instAtLeastTwoHAddOfNat real_inner_comm inner_smul_rotation_pi_div_two_left
inner_smul_rotation_pi_div_two_smul_left 📖	mathematical	—	Inner.inner Real InnerProductSpace.toInner Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace DFunLike.coe LinearIsometryEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids EquivLike.toFunLike LinearIsometryEquiv.instEquivLike rotation Real.Angle.coe DivInvMonoid.toDiv Real.instDivInvMonoid Real.pi instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.instZero	—	Real.instIsStrictOrderedRing RingHomInvPair.ids Nat.instAtLeastTwoHAddOfNat inner_smul_right inner_smul_rotation_pi_div_two_left MulZeroClass.mul_zero
inner_smul_rotation_pi_div_two_smul_right 📖	mathematical	—	Inner.inner Real InnerProductSpace.toInner Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace DFunLike.coe LinearIsometryEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids EquivLike.toFunLike LinearIsometryEquiv.instEquivLike rotation Real.Angle.coe DivInvMonoid.toDiv Real.instDivInvMonoid Real.pi instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.instZero	—	Real.instIsStrictOrderedRing RingHomInvPair.ids Nat.instAtLeastTwoHAddOfNat real_inner_comm inner_smul_rotation_pi_div_two_smul_left
kahler_rotation_left 📖	mathematical	—	DFunLike.coe LinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring Complex ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Complex.instNormedAddCommGroup NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing instInnerProductSpaceRealComplex LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self Real.instCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Real.commRing kahler LinearIsometryEquiv RingHomInvPair.ids EquivLike.toFunLike LinearIsometryEquiv.instEquivLike rotation Complex.instMul RingHom CommSemiring.toSemiring Complex.instCommSemiring RingHom.instFunLike starRingEnd Complex.instStarRing Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SeminormedRing.toRing SetLike.instMembership Submonoid.instSetLike Submonoid.unitSphere Real.Angle.toCircle	—	Real.instIsStrictOrderedRing smulCommClass_self RingHomInvPair.ids map_add SemilinearMapClass.toAddHomClass LinearMap.semilinearMapClass MulActionSemiHomClass.map_smulₛₗ SemilinearMapClass.toMulActionSemiHomClass kahler_rightAngleRotation_left Real.Angle.coe_toCircle Complex.instCharZero RingHomClass.toLinearMapClassNNRat RingHom.instRingHomClass Complex.conj_ofReal map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass Complex.conj_I Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add
kahler_rotation_left' 📖	mathematical	—	DFunLike.coe LinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring Complex ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Complex.instNormedAddCommGroup NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing instInnerProductSpaceRealComplex LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self Real.instCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Real.commRing kahler LinearIsometryEquiv RingHomInvPair.ids EquivLike.toFunLike LinearIsometryEquiv.instEquivLike rotation Complex.instMul Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SeminormedRing.toRing SetLike.instMembership Submonoid.instSetLike Submonoid.unitSphere Real.Angle.toCircle Real.Angle NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Real.instNormedAddCommGroupAngle	—	Real.instIsStrictOrderedRing smulCommClass_self RingHomInvPair.ids kahler_rotation_left Real.Angle.toCircle_neg Circle.coe_inv_eq_conj
kahler_rotation_right 📖	mathematical	—	DFunLike.coe LinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring Complex ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Complex.instNormedAddCommGroup NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing instInnerProductSpaceRealComplex LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self Real.instCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Real.commRing kahler LinearIsometryEquiv RingHomInvPair.ids EquivLike.toFunLike LinearIsometryEquiv.instEquivLike rotation Complex.instMul Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SeminormedRing.toRing SetLike.instMembership Submonoid.instSetLike Submonoid.unitSphere Real.Angle.toCircle	—	Real.instIsStrictOrderedRing smulCommClass_self RingHomInvPair.ids map_add SemilinearMapClass.toAddHomClass LinearMap.semilinearMapClass MulActionSemiHomClass.map_smulₛₗ SemilinearMapClass.toMulActionSemiHomClass kahler_rightAngleRotation_right Real.Angle.coe_toCircle Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add
linearEquiv_det_rotation 📖	mathematical	—	DFunLike.coe MonoidHom LinearEquiv Real CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid LinearEquiv.automorphismGroup Units.instMulOneClass MonoidHom.instFunLike LinearEquiv.det LinearIsometryEquiv.toLinearEquiv Real.semiring rotation Units.instOne	—	Real.instIsStrictOrderedRing Units.ext RingHomInvPair.ids det_rotation
neg_rotation 📖	mathematical	—	NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup DFunLike.coe LinearIsometryEquiv Real Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike EquivLike.toFunLike LinearIsometryEquiv.instEquivLike rotation Real.Angle AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Real.instNormedAddCommGroupAngle ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Real.Angle.coe Real.pi	—	Real.instIsStrictOrderedRing RingHomInvPair.ids rotation_pi_apply rotation_rotation
neg_rotation_neg_pi_div_two 📖	mathematical	—	NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup DFunLike.coe LinearIsometryEquiv Real Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike EquivLike.toFunLike LinearIsometryEquiv.instEquivLike rotation Real.Angle.coe DivInvMonoid.toDiv Real.instDivInvMonoid Real.instNeg Real.pi instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Real.instIsStrictOrderedRing RingHomInvPair.ids Nat.instAtLeastTwoHAddOfNat neg_rotation Real.Angle.coe_add neg_div sub_eq_add_neg sub_half CharZero.NeZero.two RCLike.charZero_rclike
neg_rotation_pi_div_two 📖	mathematical	—	NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup DFunLike.coe LinearIsometryEquiv Real Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike EquivLike.toFunLike LinearIsometryEquiv.instEquivLike rotation Real.Angle.coe DivInvMonoid.toDiv Real.instDivInvMonoid Real.pi instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.instNeg	—	Real.instIsStrictOrderedRing RingHomInvPair.ids Nat.instAtLeastTwoHAddOfNat neg_eq_iff_eq_neg neg_rotation_neg_pi_div_two
oangle_eq_iff_eq_norm_div_norm_smul_rotation_of_ne_zero 📖	mathematical	—	oangle Real SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike DivInvMonoid.toDiv Real.instDivInvMonoid Norm.norm NormedAddCommGroup.toNorm DFunLike.coe LinearIsometryEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids EquivLike.toFunLike LinearIsometryEquiv.instEquivLike rotation	—	Real.instIsStrictOrderedRing div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono norm_pos_iff RingHomInvPair.ids map_smul SemilinearMapClass.toMulActionSemiHomClass SemilinearIsometryClass.toSemilinearMapClass SemilinearIsometryEquivClass.toSemilinearIsometryClass LinearIsometryEquiv.instSemilinearIsometryEquivClass oangle_smul_left_of_pos rotation_oangle_eq_iff_norm_eq norm_smul NormedSpace.toNormSMulClass Real.norm_of_nonneg LT.lt.le div_mul_cancel₀ norm_ne_zero_iff oangle_smul_right_of_pos oangle_rotation_self_right
oangle_eq_iff_eq_norm_div_norm_smul_rotation_or_eq_zero 📖	mathematical	—	oangle Real SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike DivInvMonoid.toDiv Real.instDivInvMonoid Norm.norm NormedAddCommGroup.toNorm DFunLike.coe LinearIsometryEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids EquivLike.toFunLike LinearIsometryEquiv.instEquivLike rotation Real.Angle NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Real.instNormedAddCommGroupAngle	—	Real.instIsStrictOrderedRing RingHomInvPair.ids oangle.congr_simp oangle_zero_left norm_zero div_zero map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass SemilinearIsometryClass.toSemilinearMapClass SemilinearIsometryEquivClass.toSemilinearIsometryClass LinearIsometryEquiv.instSemilinearIsometryEquivClass smul_zero oangle_zero_right zero_div zero_smul oangle_eq_iff_eq_norm_div_norm_smul_rotation_of_ne_zero
oangle_eq_iff_eq_pos_smul_rotation_of_ne_zero 📖	mathematical	—	oangle Real Real.instLT Real.instZero SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike DFunLike.coe LinearIsometryEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids EquivLike.toFunLike LinearIsometryEquiv.instEquivLike rotation	—	Real.instIsStrictOrderedRing RingHomInvPair.ids div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono norm_pos_iff oangle_eq_iff_eq_norm_div_norm_smul_rotation_of_ne_zero oangle_smul_right_of_pos oangle_rotation_self_right
oangle_eq_iff_eq_pos_smul_rotation_or_eq_zero 📖	mathematical	—	oangle Real Real.instLT Real.instZero SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike DFunLike.coe LinearIsometryEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids EquivLike.toFunLike LinearIsometryEquiv.instEquivLike rotation Real.Angle NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Real.instNormedAddCommGroupAngle	—	Real.instIsStrictOrderedRing RingHomInvPair.ids oangle.congr_simp oangle_zero_left map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass SemilinearIsometryClass.toSemilinearMapClass SemilinearIsometryEquivClass.toSemilinearIsometryClass LinearIsometryEquiv.instSemilinearIsometryEquivClass smul_zero oangle_zero_right oangle_eq_iff_eq_pos_smul_rotation_of_ne_zero
oangle_rotation 📖	mathematical	—	oangle DFunLike.coe LinearIsometryEquiv Real Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike EquivLike.toFunLike LinearIsometryEquiv.instEquivLike rotation	—	Real.instIsStrictOrderedRing RingHomInvPair.ids oangle.congr_simp map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass SemilinearIsometryClass.toSemilinearMapClass SemilinearIsometryEquivClass.toSemilinearIsometryClass LinearIsometryEquiv.instSemilinearIsometryEquivClass oangle_self oangle_zero_left oangle_zero_right oangle_rotation_right EquivLike.toEmbeddingLike oangle_rotation_left sub_add_cancel
oangle_rotation_left 📖	mathematical	—	oangle DFunLike.coe LinearIsometryEquiv Real Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike EquivLike.toFunLike LinearIsometryEquiv.instEquivLike rotation Real.Angle SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Real.instNormedAddCommGroupAngle	—	Real.instIsStrictOrderedRing RingHomInvPair.ids smulCommClass_self kahler_rotation_left' Complex.arg_mul_coe_angle Circle.coe_ne_zero kahler_ne_zero Real.Angle.arg_toCircle Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.subst_into_negg Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.term_neg neg_zero Mathlib.Tactic.Abel.term_add_constg zero_add Mathlib.Tactic.Abel.unfold_sub Mathlib.Tactic.Abel.const_add_termg add_zero
oangle_rotation_oangle_left 📖	mathematical	—	oangle DFunLike.coe LinearIsometryEquiv Real Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike EquivLike.toFunLike LinearIsometryEquiv.instEquivLike rotation Real.Angle NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Real.instNormedAddCommGroupAngle	—	Real.instIsStrictOrderedRing RingHomInvPair.ids oangle.congr_simp rotation.congr_simp oangle_zero_left rotation_zero oangle_zero_right oangle_rotation_left sub_self
oangle_rotation_oangle_right 📖	mathematical	—	oangle DFunLike.coe LinearIsometryEquiv Real Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike EquivLike.toFunLike LinearIsometryEquiv.instEquivLike rotation Real.Angle NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Real.instNormedAddCommGroupAngle	—	Real.instIsStrictOrderedRing RingHomInvPair.ids oangle_rev oangle_rotation_oangle_left neg_zero
oangle_rotation_right 📖	mathematical	—	oangle DFunLike.coe LinearIsometryEquiv Real Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike EquivLike.toFunLike LinearIsometryEquiv.instEquivLike rotation Real.Angle AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Real.instNormedAddCommGroupAngle ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	Real.instIsStrictOrderedRing RingHomInvPair.ids smulCommClass_self kahler_rotation_right Complex.arg_mul_coe_angle Circle.coe_ne_zero kahler_ne_zero Real.Angle.arg_toCircle Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.term_add_constg zero_add Mathlib.Tactic.Abel.const_add_termg add_zero
oangle_rotation_self_left 📖	mathematical	—	oangle DFunLike.coe LinearIsometryEquiv Real Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike EquivLike.toFunLike LinearIsometryEquiv.instEquivLike rotation Real.Angle NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Real.instNormedAddCommGroupAngle	—	Real.instIsStrictOrderedRing RingHomInvPair.ids oangle_rotation_left oangle_self zero_sub
oangle_rotation_self_right 📖	mathematical	—	oangle DFunLike.coe LinearIsometryEquiv Real Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike EquivLike.toFunLike LinearIsometryEquiv.instEquivLike rotation	—	Real.instIsStrictOrderedRing RingHomInvPair.ids oangle_rotation_right oangle_self zero_add
rotationAux_apply 📖	mathematical	—	DFunLike.coe LinearIsometry Real Real.semiring RingHom.id Semiring.toNonAssocSemiring NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike LinearIsometry.instFunLike rotationAux AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.Angle.cos Real.Angle.sin LinearIsometryEquiv RingHomInvPair.ids EquivLike.toFunLike LinearIsometryEquiv.instEquivLike rightAngleRotation	—	Real.instIsStrictOrderedRing
rotation_apply 📖	mathematical	—	DFunLike.coe LinearIsometryEquiv Real Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike EquivLike.toFunLike LinearIsometryEquiv.instEquivLike rotation AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.Angle.cos Real.Angle.sin rightAngleRotation	—	Real.instIsStrictOrderedRing RingHomInvPair.ids
rotation_eq_matrix_toLin 📖	mathematical	—	LinearEquiv.toLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike LinearIsometryEquiv.toLinearEquiv rotation DFunLike.coe LinearEquiv CommSemiring.toSemiring Real.instCommSemiring Matrix LinearMap ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Matrix.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring LinearMap.addCommMonoid Matrix.module Semiring.toModule LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Matrix.toLin Fin.fintype Finite.of_fintype basisRightAngleRotation Equiv Equiv.instEquivLike Matrix.of Matrix.vecCons Real.Angle.cos Real.instNeg Real.Angle.sin Matrix.vecEmpty	—	Real.instIsStrictOrderedRing Module.Basis.ext RingHomInvPair.ids smulCommClass_self Finite.of_fintype Fintype.complete Matrix.toLin_self coe_basisRightAngleRotation Finset.sum_congr Matrix.cons_val' Matrix.cons_val_fin_one Fin.sum_univ_succ Finset.univ_unique Matrix.cons_val_succ Finset.sum_const Finset.card_singleton one_smul rightAngleRotation_rightAngleRotation smul_neg add_comm neg_smul
rotation_eq_self_iff 📖	mathematical	—	DFunLike.coe LinearIsometryEquiv Real Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike EquivLike.toFunLike LinearIsometryEquiv.instEquivLike rotation NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Real.Angle Real.instNormedAddCommGroupAngle	—	Real.instIsStrictOrderedRing RingHomInvPair.ids map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass SemilinearIsometryClass.toSemilinearMapClass SemilinearIsometryEquivClass.toSemilinearIsometryClass LinearIsometryEquiv.instSemilinearIsometryEquivClass
rotation_eq_self_iff_angle_eq_zero 📖	mathematical	—	DFunLike.coe LinearIsometryEquiv Real Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike EquivLike.toFunLike LinearIsometryEquiv.instEquivLike rotation Real.Angle NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Real.instNormedAddCommGroupAngle	—	Real.instIsStrictOrderedRing RingHomInvPair.ids oangle.congr_simp oangle_self zero_add oangle_rotation_right rotation.congr_simp rotation_zero
rotation_map 📖	mathematical	—	DFunLike.coe LinearIsometryEquiv Real Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike EquivLike.toFunLike LinearIsometryEquiv.instEquivLike rotation Equiv Orientation Real.instCommSemiring Real.partialOrder Real.instIsStrictOrderedRing AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup Equiv.instEquivLike map LinearIsometryEquiv.toLinearEquiv LinearIsometryEquiv.symm	—	Real.instIsStrictOrderedRing RingHomInvPair.ids rightAngleRotation_map map_add SemilinearMapClass.toAddHomClass SemilinearIsometryClass.toSemilinearMapClass SemilinearIsometryEquivClass.toSemilinearIsometryClass LinearIsometryEquiv.instSemilinearIsometryEquivClass map_smul SemilinearMapClass.toMulActionSemiHomClass LinearIsometryEquiv.apply_symm_apply
rotation_map_complex 📖	mathematical	DFunLike.coe Equiv Orientation Real Real.instCommSemiring Real.partialOrder Real.instIsStrictOrderedRing AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike Complex NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField instInnerProductSpaceRealComplex EquivLike.toFunLike Equiv.instEquivLike map LinearIsometryEquiv.toLinearEquiv Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Complex.orientation	LinearIsometryEquiv LinearIsometryEquiv.instEquivLike rotation Complex.instMul Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Ring.toSemiring SeminormedRing.toRing SeminormedCommRing.toSeminormedRing SetLike.instMembership Submonoid.instSetLike Submonoid.unitSphere Real.Angle.toCircle	—	Real.instIsStrictOrderedRing RingHomInvPair.ids Complex.finrank_real_complex_fact Complex.rotation rotation_map LinearIsometryEquiv.symm_apply_apply
rotation_neg_orientation_eq_neg 📖	mathematical	—	rotation Orientation Real Real.instCommSemiring Real.partialOrder Real.instIsStrictOrderedRing ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike instNegRay Real.commRing AlternatingMap CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule AlternatingMap.instAddCommGroup Real.instAddCommGroup AlternatingMap.instModule Real.Angle NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Real.instNormedAddCommGroupAngle	—	Real.instIsStrictOrderedRing LinearIsometryEquiv.ext RingHomInvPair.ids RingHomCompTriple.ids rightAngleRotation_trans_neg_orientation smul_neg Real.Angle.cos_neg Real.Angle.sin_neg neg_smul
rotation_oangle_eq_iff_norm_eq 📖	mathematical	—	DFunLike.coe LinearIsometryEquiv Real Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike EquivLike.toFunLike LinearIsometryEquiv.instEquivLike rotation oangle Norm.norm NormedAddCommGroup.toNorm	—	Real.instIsStrictOrderedRing RingHomInvPair.ids LinearIsometryEquiv.norm_map eq_iff_oangle_eq_zero_of_norm_eq oangle_rotation_oangle_left
rotation_pi 📖	mathematical	—	rotation Real.Angle.coe Real.pi LinearIsometryEquiv.neg Real Real.semiring NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike	—	Real.instIsStrictOrderedRing LinearIsometryEquiv.ext RingHomInvPair.ids RingHomInvPair.triples₂ smulCommClass_self Real.cos_pi neg_smul one_smul Real.sin_pi zero_smul sub_zero LinearIsometryEquiv.ofLinearIsometry.congr_simp add_zero
rotation_pi_apply 📖	mathematical	—	DFunLike.coe LinearIsometryEquiv Real Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike EquivLike.toFunLike LinearIsometryEquiv.instEquivLike rotation Real.Angle.coe Real.pi NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	Real.instIsStrictOrderedRing RingHomInvPair.ids rotation_pi
rotation_pi_div_two 📖	mathematical	—	rotation Real.Angle.coe Real DivInvMonoid.toDiv Real.instDivInvMonoid Real.pi instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat rightAngleRotation	—	Real.instIsStrictOrderedRing LinearIsometryEquiv.ext RingHomInvPair.ids Nat.instAtLeastTwoHAddOfNat RingHomInvPair.triples₂ Real.cos_pi_div_two zero_smul smulCommClass_self Real.sin_pi_div_two one_smul zero_sub LinearIsometryEquiv.ofLinearIsometry.congr_simp zero_add
rotation_rotation 📖	mathematical	—	DFunLike.coe LinearIsometryEquiv Real Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike EquivLike.toFunLike LinearIsometryEquiv.instEquivLike rotation Real.Angle AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Real.instNormedAddCommGroupAngle ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	Real.instIsStrictOrderedRing RingHomInvPair.ids map_add SemilinearMapClass.toAddHomClass SemilinearIsometryClass.toSemilinearMapClass SemilinearIsometryEquivClass.toSemilinearIsometryClass LinearIsometryEquiv.instSemilinearIsometryEquivClass map_smul SemilinearMapClass.toMulActionSemiHomClass rightAngleRotation_rightAngleRotation Real.Angle.cos_add Real.Angle.sin_add Mathlib.Tactic.Module.NF.eq_of_eval_eq_eval Mathlib.Tactic.Module.NF.add_eq_eval Mathlib.Tactic.Module.NF.smul_eq_eval Mathlib.Tactic.Module.NF.atom_eq_eval Mathlib.Tactic.Module.NF.eval_algebraMap AddCommMonoid.nat_isScalarTower Mathlib.Tactic.Module.NF.add_eq_eval₁ zero_add Mathlib.Tactic.Module.NF.neg_eq_eval AddCommGroup.intIsScalarTower Mathlib.Tactic.Module.NF.add_eq_eval₃ add_zero Mathlib.Tactic.Module.NF.add_eq_eval₂ Mathlib.Tactic.Module.NF.eq_cons_cons eq_natCast RingHom.instRingHomClass Nat.cast_one eq_intCast Int.cast_neg Int.cast_one Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.add_pf_add_gt
rotation_symm 📖	mathematical	—	LinearIsometryEquiv.symm Real Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike rotation Real.Angle NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Real.instNormedAddCommGroupAngle	—	Real.instIsStrictOrderedRing LinearIsometryEquiv.ext RingHomInvPair.ids sub_eq_add_neg Real.Angle.cos_neg Real.Angle.sin_neg neg_smul
rotation_symm_apply 📖	mathematical	—	DFunLike.coe LinearIsometryEquiv Real Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike EquivLike.toFunLike LinearIsometryEquiv.instEquivLike LinearIsometryEquiv.symm rotation SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid Real.Angle.cos Real.Angle.sin rightAngleRotation	—	Real.instIsStrictOrderedRing RingHomInvPair.ids
rotation_trans 📖	mathematical	—	LinearIsometryEquiv.trans Real Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids RingHomCompTriple.ids NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike rotation Real.Angle AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Real.instNormedAddCommGroupAngle ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	Real.instIsStrictOrderedRing LinearIsometryEquiv.ext RingHomInvPair.ids RingHomCompTriple.ids rotation_rotation LinearIsometryEquiv.trans_apply
rotation_zero 📖	mathematical	—	rotation Real.Angle NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Real.instNormedAddCommGroupAngle LinearIsometryEquiv.refl Real Real.semiring NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike	—	Real.instIsStrictOrderedRing LinearIsometryEquiv.ext RingHomInvPair.ids RingHomInvPair.triples₂ Real.Angle.cos_zero one_smul smulCommClass_self Real.Angle.sin_zero zero_smul sub_zero LinearIsometryEquiv.ofLinearIsometry.congr_simp add_zero

---

← Back to Index