| Name | Category | Theorems |
|---|
Angle 📖 | CompOp | 221 mathmath: Angle.abs_toReal_neg_coe_eq_self_iff, Orientation.oangle_eq_zero_or_eq_pi_iff_right_eq_smul, Orientation.oangle_add, Angle.sign_two_zsmul_eq_sign_iff, Angle.neg_coe_abs_toReal_of_sign_nonpos, Angle.toReal_add_of_sign_eq_neg_sign, Orientation.oangle_add_swap, EuclideanGeometry.two_zsmul_oangle_of_parallel, EuclideanGeometry.oangle_eq_neg_of_angle_eq_of_sign_eq_neg, Angle.two_zsmul_eq_pi_iff, Orientation.oangle_eq_zero_iff_oangle_rev_eq_zero, Angle.sin_add_pi_div_two, Angle.cos_add, Orientation.eq_iff_norm_eq_and_oangle_eq_zero, Orientation.oangle_eq_two_zsmul_oangle_sub_of_norm_eq, Angle.cos_zero, Orientation.rotation_eq_self_iff, Angle.sign_neg_coe_nonpos_of_nonneg_of_le_pi, Orientation.two_zsmul_oangle_smul_left_of_ne_zero, EuclideanGeometry.oangle_eq_pi_sub_two_zsmul_oangle_of_dist_eq, Angle.toCircle_add, Angle.sin_eq_zero_iff, Angle.sign_neg, Orientation.neg_rotation, Sbtw.oangle_eq_add_pi_left, Orientation.eq_rotation_self_iff_angle_eq_zero, Orientation.two_zsmul_oangle_neg_left, Orientation.oangle_zero_left, EuclideanGeometry.oangle_eq_angle_or_eq_neg_angle, Angle.two_zsmul_eq_iff_eq, Angle.cos_eq_real_cos_iff_eq_or_eq_neg, EuclideanGeometry.oangle_self_left_right, Orientation.two_zsmul_oangle_neg_self_right, Orientation.oangle_neg_right, Angle.continuousAt_sign, Angle.two_zsmul_coe_div_two, Wbtw.oangle₃₁₂_eq_zero, EuclideanGeometry.oangle_rev, Angle.sign_two_nsmul_eq_neg_sign_iff, Angle.sign_pi_sub, EuclideanGeometry.oangle_eq_zero_iff_angle_eq_zero, Orientation.oangle_smul_left_self_of_nonneg, Angle.sign_eq_zero_iff, Wbtw.oangle₂₁₃_eq_zero, Orientation.rotation_rotation, Angle.two_nsmul_toReal_eq_two_mul_sub_two_pi, EuclideanGeometry.Sphere.oangle_eq_pi_sub_two_zsmul_oangle_center_left, EuclideanGeometry.oangle_add, Orientation.oangle_eq_angle_or_eq_neg_angle, EuclideanGeometry.oangle_eq_zero_iff_oangle_rev_eq_zero, Angle.sin_add_pi, Angle.sin_neg, Angle.cos_add_pi, EuclideanGeometry.oangle_add_swap, Angle.two_zsmul_coe_pi, Angle.cos_add_pi_div_two, Angle.two_nsmul_eq_zero_iff, Angle.coe_add, Angle.abs_toReal_neg, Orientation.rotation_symm, Sbtw.oangle₂₃₁_eq_zero, Sbtw.oangle_eq_add_pi_right, Orientation.oangle_eq_zero_iff_sameRay, Orientation.oangle_rotation_left, Angle.sign_zero, Angle.coe_eq_zero_iff, Angle.coe_coeHom, Angle.toReal_neg_eq_neg_toReal_iff, Angle.toCircle_zero, EuclideanGeometry.oangle_eq_zero_iff_wbtw, Angle.two_zsmul_toReal_eq_two_mul_sub_two_pi, Angle.cos_sub_pi, Orientation.oangle_eq_zero_iff_angle_eq_zero, Orientation.oangle_rotation_oangle_right, EuclideanGeometry.oangle_add_cyc3, Orientation.oangle_add_oangle_rev, Orientation.oangle_self, Angle.tan_sub_pi, EuclideanGeometry.oangle_sub_left, Angle.sub_coe_pi_eq_add_coe_pi, Angle.sin_eq_iff_coe_eq_or_add_eq_pi, Angle.sign_sub_pi, Orientation.oangle_rotation_self_left, Angle.sin_two_nsmul, EuclideanGeometry.two_zsmul_oangle_self_orthogonalProjection, Angle.two_zsmul_neg_pi_div_two, Angle.two_nsmul_eq_iff_eq_of_abs_toReal_lt_pi_div_two, Orientation.rotation_neg_orientation_eq_neg, Orientation.eq_rotation_self_iff, Angle.two_zsmul_toReal_eq_two_mul, Orientation.two_zsmul_oangle_of_span_eq_of_span_eq, Collinear.two_zsmul_oangle_eq_right, Orientation.oangle_eq_iff_eq_pos_smul_rotation_or_eq_zero, Orientation.rotation_zero, Orientation.oangle_neg_left, Orientation.oangle_rotation_oangle_left, Angle.coe_sub, Angle.intCast_mul_eq_zsmul, EuclideanGeometry.oangle_add_oangle_add_oangle_eq_pi, EuclideanGeometry.oangle_eq_zero_or_eq_pi_iff_collinear, Angle.cos_eq_iff_coe_eq_or_eq_neg, Angle.two_zsmul_eq_iff_eq_of_abs_toReal_lt_pi_div_two, Orientation.oangle_zero_right, Orientation.rotation_eq_self_iff_angle_eq_zero, Orientation.oangle_rotation_right, Orientation.oangle_sub_left, Angle.sign_two_nsmul_eq_sign_iff, Orientation.rotation_trans, Orientation.continuousAt_oangle, Angle.sin_pi_div_two_sub, Angle.sin_add, Angle.toReal_injective, Angle.two_zsmul_eq_iff, Orientation.oangle_add_cyc3, EuclideanGeometry.continuousAt_oangle, Angle.two_nsmul_toReal_eq_two_mul_add_two_pi, Angle.sign_pi_add, Angle.two_nsmul_eq_pi_iff, EuclideanGeometry.oangle_self_right, Orientation.kahler_rotation_left', Orientation.oangle_eq_zero_or_eq_pi_iff_not_linearIndependent, Angle.sign_two_zsmul_eq_neg_sign_iff, Complex.continuousAt_arg_coe_angle, Complex.arg_div_coe_angle, Angle.two_zsmul_toReal_eq_two_mul_add_two_pi, Orientation.oangle_eq_iff_eq_norm_div_norm_smul_rotation_or_eq_zero, Wbtw.oangle₂₃₁_eq_zero, Angle.continuous_coe, EuclideanGeometry.Sphere.oangle_eq_pi_sub_two_zsmul_oangle_center_right, Angle.toReal_eq_zero_iff, Sbtw.oangle₃₁₂_eq_zero, Angle.sin_eq_iff_eq_or_add_eq_pi, Orientation.two_zsmul_oangle_neg_self_left, Orientation.oangle_eq_pi_sub_two_zsmul_oangle_sub_of_norm_eq, EuclideanGeometry.angle_eq_iff_oangle_eq_neg_of_sign_eq_neg, Angle.coe_nsmul, Angle.sign_add_pi, Angle.toReal_add_of_sign_pos_sign_neg, Complex.arg_conj_coe_angle, Angle.natCast_mul_eq_nsmul, Angle.zsmul_eq_iff, Orientation.oangle_add_cyc3_neg_left, EuclideanGeometry.oangle_eq_or_eq_neg_of_angle_eq, Sbtw.oangle₁₃₂_eq_zero, Angle.eq_neg_self_iff, Sbtw.oangle₂₁₃_eq_zero, Orientation.oangle_smul_smul_self_of_nonneg, EuclideanGeometry.oangle_add_oangle_rev, Angle.neg_coe_pi, Orientation.two_zsmul_oangle_smul_right_self, Angle.two_nsmul_coe_div_two, Angle.neg_eq_self_iff, Angle.toCircle_neg, EuclideanGeometry.Sphere.two_zsmul_oangle_eq, EuclideanGeometry.Sphere.two_zsmul_oangle_center_add_two_zsmul_oangle_eq_pi, Angle.continuous_sin, Orientation.oangle_rev, Angle.sin_zero, Orientation.oangle_add_oangle_rev_neg_left, Orientation.two_zsmul_oangle_neg_right, Angle.cos_pi_div_two_sub, Orientation.two_zsmul_oangle_sub_eq_two_zsmul_oangle_sub_of_norm_eq, EuclideanGeometry.Sphere.oangle_center_eq_two_zsmul_oangle, Angle.cos_eq_iff_eq_or_eq_neg, Orientation.two_zsmul_oangle_smul_right_of_ne_zero, Orientation.eq_iff_oangle_eq_zero_of_norm_eq, Orientation.oangle_smul_add_right_eq_zero_or_eq_pi_iff, Angle.coe_two_pi, Angle.coe_zsmul, Orientation.two_zsmul_oangle_left_of_span_eq, Orientation.two_zsmul_oangle_smul_left_self, Complex.arg_pow_coe_angle, Orientation.angle_eq_iff_oangle_eq_neg_of_sign_eq_neg, Angle.nsmul_toReal_eq_mul, Orientation.oangle_eq_neg_of_angle_eq_of_sign_eq_neg, Angle.coe_zero, Collinear.two_zsmul_oangle_eq_left, EuclideanGeometry.Cospherical.two_zsmul_oangle_eq, EuclideanGeometry.oangle_self_left, Angle.abs_toReal_add_eq_two_pi_sub_abs_toReal_add_abs_toReal, Complex.arg_inv_coe_angle, Angle.cos_neg, Angle.cos_sub_pi_div_two, Angle.two_zsmul_eq_zero_iff, EuclideanGeometry.two_zsmul_oangle_eq_of_dist_orthogonalProjection_line_eq, Angle.two_nsmul_neg_pi_div_two, Angle.tan_add_pi, Angle.sin_antiperiodic, EuclideanGeometry.two_zsmul_oangle_orthogonalProjection_self, Angle.two_nsmul_coe_pi, EuclideanGeometry.two_zsmul_oangle_of_vectorSpan_eq, Orientation.oangle_smul_right_self_of_nonneg, Orientation.oangle_eq_two_zsmul_oangle_sub_of_norm_eq_real, Complex.arg_mul_coe_angle, Orientation.oangle_neg_orientation_eq_neg, Angle.sin_eq_real_sin_iff_eq_or_add_eq_pi, Orientation.oangle_sub_right, Angle.cos_antiperiodic, EuclideanGeometry.oangle_eq_neg_angle_of_sign_eq_neg_one, Orientation.two_zsmul_oangle_smul_smul_self, Angle.sin_sub_pi_div_two, EuclideanGeometry.oangle_sub_right, Wbtw.oangle₁₃₂_eq_zero, EuclideanGeometry.dist_orthogonalProjection_line_eq_iff_two_zsmul_oangle_eq, Angle.continuous_cos, Angle.tan_periodic, Angle.coe_pi_add_coe_pi, Orientation.oangle_eq_neg_angle_of_sign_eq_neg_one, Orientation.oangle_add_cyc3_neg_right, Complex.arg_zpow_coe_angle, Angle.tan_zero, Angle.two_nsmul_eq_iff, Orientation.two_zsmul_oangle_right_of_span_eq, Angle.two_nsmul_toReal_eq_two_mul, Angle.sign_antiperiodic, Angle.nsmul_eq_iff, Angle.toReal_zero, Angle.sin_sub_pi, Complex.arg_neg_coe_angle, Angle.coe_neg, Orientation.oangle_add_oangle_rev_neg_right
|
instInhabitedAngle 📖 | CompOp | — |
instNormedAddCommGroupAngle 📖 | CompOp | 220 mathmath: Angle.abs_toReal_neg_coe_eq_self_iff, Orientation.oangle_eq_zero_or_eq_pi_iff_right_eq_smul, Orientation.oangle_add, Angle.sign_two_zsmul_eq_sign_iff, Angle.neg_coe_abs_toReal_of_sign_nonpos, Angle.toReal_add_of_sign_eq_neg_sign, Orientation.oangle_add_swap, EuclideanGeometry.two_zsmul_oangle_of_parallel, EuclideanGeometry.oangle_eq_neg_of_angle_eq_of_sign_eq_neg, Angle.two_zsmul_eq_pi_iff, Orientation.oangle_eq_zero_iff_oangle_rev_eq_zero, Angle.sin_add_pi_div_two, Angle.cos_add, Orientation.eq_iff_norm_eq_and_oangle_eq_zero, Orientation.oangle_eq_two_zsmul_oangle_sub_of_norm_eq, Angle.cos_zero, Orientation.rotation_eq_self_iff, Angle.sign_neg_coe_nonpos_of_nonneg_of_le_pi, Orientation.two_zsmul_oangle_smul_left_of_ne_zero, EuclideanGeometry.oangle_eq_pi_sub_two_zsmul_oangle_of_dist_eq, Angle.toCircle_add, Angle.sin_eq_zero_iff, Angle.sign_neg, Orientation.neg_rotation, Sbtw.oangle_eq_add_pi_left, Orientation.eq_rotation_self_iff_angle_eq_zero, Orientation.two_zsmul_oangle_neg_left, Orientation.oangle_zero_left, EuclideanGeometry.oangle_eq_angle_or_eq_neg_angle, Angle.two_zsmul_eq_iff_eq, Angle.cos_eq_real_cos_iff_eq_or_eq_neg, EuclideanGeometry.oangle_self_left_right, Orientation.two_zsmul_oangle_neg_self_right, Orientation.oangle_neg_right, Angle.continuousAt_sign, Angle.two_zsmul_coe_div_two, Wbtw.oangle₃₁₂_eq_zero, EuclideanGeometry.oangle_rev, Angle.sign_two_nsmul_eq_neg_sign_iff, Angle.sign_pi_sub, EuclideanGeometry.oangle_eq_zero_iff_angle_eq_zero, Orientation.oangle_smul_left_self_of_nonneg, Angle.sign_eq_zero_iff, Wbtw.oangle₂₁₃_eq_zero, Orientation.rotation_rotation, Angle.two_nsmul_toReal_eq_two_mul_sub_two_pi, EuclideanGeometry.Sphere.oangle_eq_pi_sub_two_zsmul_oangle_center_left, EuclideanGeometry.oangle_add, Orientation.oangle_eq_angle_or_eq_neg_angle, EuclideanGeometry.oangle_eq_zero_iff_oangle_rev_eq_zero, Angle.sin_add_pi, Angle.sin_neg, Angle.cos_add_pi, EuclideanGeometry.oangle_add_swap, Angle.two_zsmul_coe_pi, Angle.cos_add_pi_div_two, Angle.two_nsmul_eq_zero_iff, Angle.coe_add, Angle.abs_toReal_neg, Orientation.rotation_symm, Sbtw.oangle₂₃₁_eq_zero, Sbtw.oangle_eq_add_pi_right, Orientation.oangle_eq_zero_iff_sameRay, Orientation.oangle_rotation_left, Angle.sign_zero, Angle.coe_eq_zero_iff, Angle.coe_coeHom, Angle.toReal_neg_eq_neg_toReal_iff, Angle.toCircle_zero, EuclideanGeometry.oangle_eq_zero_iff_wbtw, Angle.two_zsmul_toReal_eq_two_mul_sub_two_pi, Angle.cos_sub_pi, Orientation.oangle_eq_zero_iff_angle_eq_zero, Orientation.oangle_rotation_oangle_right, EuclideanGeometry.oangle_add_cyc3, Orientation.oangle_add_oangle_rev, Orientation.oangle_self, Angle.tan_sub_pi, EuclideanGeometry.oangle_sub_left, Angle.sub_coe_pi_eq_add_coe_pi, Angle.sin_eq_iff_coe_eq_or_add_eq_pi, Angle.sign_sub_pi, Orientation.oangle_rotation_self_left, Angle.sin_two_nsmul, EuclideanGeometry.two_zsmul_oangle_self_orthogonalProjection, Angle.two_zsmul_neg_pi_div_two, Angle.two_nsmul_eq_iff_eq_of_abs_toReal_lt_pi_div_two, Orientation.rotation_neg_orientation_eq_neg, Orientation.eq_rotation_self_iff, Angle.two_zsmul_toReal_eq_two_mul, Orientation.two_zsmul_oangle_of_span_eq_of_span_eq, Collinear.two_zsmul_oangle_eq_right, Orientation.oangle_eq_iff_eq_pos_smul_rotation_or_eq_zero, Orientation.rotation_zero, Orientation.oangle_neg_left, Orientation.oangle_rotation_oangle_left, Angle.coe_sub, Angle.intCast_mul_eq_zsmul, EuclideanGeometry.oangle_add_oangle_add_oangle_eq_pi, EuclideanGeometry.oangle_eq_zero_or_eq_pi_iff_collinear, Angle.cos_eq_iff_coe_eq_or_eq_neg, Angle.two_zsmul_eq_iff_eq_of_abs_toReal_lt_pi_div_two, Orientation.oangle_zero_right, Orientation.rotation_eq_self_iff_angle_eq_zero, Orientation.oangle_rotation_right, Orientation.oangle_sub_left, Angle.sign_two_nsmul_eq_sign_iff, Orientation.rotation_trans, Orientation.continuousAt_oangle, Angle.sin_pi_div_two_sub, Angle.sin_add, Angle.two_zsmul_eq_iff, Orientation.oangle_add_cyc3, EuclideanGeometry.continuousAt_oangle, Angle.two_nsmul_toReal_eq_two_mul_add_two_pi, Angle.sign_pi_add, Angle.two_nsmul_eq_pi_iff, EuclideanGeometry.oangle_self_right, Orientation.kahler_rotation_left', Orientation.oangle_eq_zero_or_eq_pi_iff_not_linearIndependent, Angle.sign_two_zsmul_eq_neg_sign_iff, Complex.continuousAt_arg_coe_angle, Complex.arg_div_coe_angle, Angle.two_zsmul_toReal_eq_two_mul_add_two_pi, Orientation.oangle_eq_iff_eq_norm_div_norm_smul_rotation_or_eq_zero, Wbtw.oangle₂₃₁_eq_zero, Angle.continuous_coe, EuclideanGeometry.Sphere.oangle_eq_pi_sub_two_zsmul_oangle_center_right, Angle.toReal_eq_zero_iff, Sbtw.oangle₃₁₂_eq_zero, Angle.sin_eq_iff_eq_or_add_eq_pi, Orientation.two_zsmul_oangle_neg_self_left, Orientation.oangle_eq_pi_sub_two_zsmul_oangle_sub_of_norm_eq, EuclideanGeometry.angle_eq_iff_oangle_eq_neg_of_sign_eq_neg, Angle.coe_nsmul, Angle.sign_add_pi, Angle.toReal_add_of_sign_pos_sign_neg, Complex.arg_conj_coe_angle, Angle.natCast_mul_eq_nsmul, Angle.zsmul_eq_iff, Orientation.oangle_add_cyc3_neg_left, EuclideanGeometry.oangle_eq_or_eq_neg_of_angle_eq, Sbtw.oangle₁₃₂_eq_zero, Angle.eq_neg_self_iff, Sbtw.oangle₂₁₃_eq_zero, Orientation.oangle_smul_smul_self_of_nonneg, EuclideanGeometry.oangle_add_oangle_rev, Angle.neg_coe_pi, Orientation.two_zsmul_oangle_smul_right_self, Angle.two_nsmul_coe_div_two, Angle.neg_eq_self_iff, Angle.toCircle_neg, EuclideanGeometry.Sphere.two_zsmul_oangle_eq, EuclideanGeometry.Sphere.two_zsmul_oangle_center_add_two_zsmul_oangle_eq_pi, Angle.continuous_sin, Orientation.oangle_rev, Angle.sin_zero, Orientation.oangle_add_oangle_rev_neg_left, Orientation.two_zsmul_oangle_neg_right, Angle.cos_pi_div_two_sub, Orientation.two_zsmul_oangle_sub_eq_two_zsmul_oangle_sub_of_norm_eq, EuclideanGeometry.Sphere.oangle_center_eq_two_zsmul_oangle, Angle.cos_eq_iff_eq_or_eq_neg, Orientation.two_zsmul_oangle_smul_right_of_ne_zero, Orientation.eq_iff_oangle_eq_zero_of_norm_eq, Orientation.oangle_smul_add_right_eq_zero_or_eq_pi_iff, Angle.coe_two_pi, Angle.coe_zsmul, Orientation.two_zsmul_oangle_left_of_span_eq, Orientation.two_zsmul_oangle_smul_left_self, Complex.arg_pow_coe_angle, Orientation.angle_eq_iff_oangle_eq_neg_of_sign_eq_neg, Angle.nsmul_toReal_eq_mul, Orientation.oangle_eq_neg_of_angle_eq_of_sign_eq_neg, Angle.coe_zero, Collinear.two_zsmul_oangle_eq_left, EuclideanGeometry.Cospherical.two_zsmul_oangle_eq, EuclideanGeometry.oangle_self_left, Angle.abs_toReal_add_eq_two_pi_sub_abs_toReal_add_abs_toReal, Complex.arg_inv_coe_angle, Angle.cos_neg, Angle.cos_sub_pi_div_two, Angle.two_zsmul_eq_zero_iff, EuclideanGeometry.two_zsmul_oangle_eq_of_dist_orthogonalProjection_line_eq, Angle.two_nsmul_neg_pi_div_two, Angle.tan_add_pi, Angle.sin_antiperiodic, EuclideanGeometry.two_zsmul_oangle_orthogonalProjection_self, Angle.two_nsmul_coe_pi, EuclideanGeometry.two_zsmul_oangle_of_vectorSpan_eq, Orientation.oangle_smul_right_self_of_nonneg, Orientation.oangle_eq_two_zsmul_oangle_sub_of_norm_eq_real, Complex.arg_mul_coe_angle, Orientation.oangle_neg_orientation_eq_neg, Angle.sin_eq_real_sin_iff_eq_or_add_eq_pi, Orientation.oangle_sub_right, Angle.cos_antiperiodic, EuclideanGeometry.oangle_eq_neg_angle_of_sign_eq_neg_one, Orientation.two_zsmul_oangle_smul_smul_self, Angle.sin_sub_pi_div_two, EuclideanGeometry.oangle_sub_right, Wbtw.oangle₁₃₂_eq_zero, EuclideanGeometry.dist_orthogonalProjection_line_eq_iff_two_zsmul_oangle_eq, Angle.continuous_cos, Angle.tan_periodic, Angle.coe_pi_add_coe_pi, Orientation.oangle_eq_neg_angle_of_sign_eq_neg_one, Orientation.oangle_add_cyc3_neg_right, Complex.arg_zpow_coe_angle, Angle.tan_zero, Angle.two_nsmul_eq_iff, Orientation.two_zsmul_oangle_right_of_span_eq, Angle.two_nsmul_toReal_eq_two_mul, Angle.sign_antiperiodic, Angle.nsmul_eq_iff, Angle.toReal_zero, Angle.sin_sub_pi, Complex.arg_neg_coe_angle, Angle.coe_neg, Orientation.oangle_add_oangle_rev_neg_right
|
| Name | Category | Theorems |
|---|
coeHom 📖 | CompOp | 1 mathmath: coe_coeHom
|
cos 📖 | CompOp | 61 mathmath: sin_add_pi_div_two, cos_add, cos_zero, Complex.arg_cos_add_sin_mul_I_coe_angle, cos_eq_real_cos_iff_eq_or_eq_neg, Orientation.norm_div_cos_oangle_add_left_of_oangle_eq_pi_div_two, abs_cos_eq_abs_sin_of_two_zsmul_add_two_zsmul_eq_pi, cos_sq_add_sin_sq, cos_add_pi, cos_add_pi_div_two, cos_nonneg_iff_abs_toReal_le_pi_div_two, coe_toCircle, Orientation.cos_oangle_sub_right_of_oangle_eq_pi_div_two, cos_sub_pi, Orientation.cos_oangle_add_left_of_oangle_eq_pi_div_two, Orientation.cos_oangle_add_right_mul_norm_of_oangle_eq_pi_div_two, EuclideanGeometry.cos_oangle_eq_cos_angle, Complex.arg_mul_cos_add_sin_mul_I_coe_angle, sin_two_nsmul, Orientation.inner_eq_norm_mul_norm_mul_cos_oangle, abs_cos_eq_abs_sin_of_two_nsmul_add_two_nsmul_eq_pi, Orientation.cos_oangle_sub_right_mul_norm_of_oangle_eq_pi_div_two, EuclideanGeometry.cos_oangle_left_mul_dist_of_oangle_eq_pi_div_two, Orientation.norm_div_cos_oangle_add_right_of_oangle_eq_pi_div_two, EuclideanGeometry.Sphere.dist_div_cos_oangle_center_div_two_eq_radius, cos_eq_zero_iff, EuclideanGeometry.cos_oangle_left_of_oangle_eq_pi_div_two, sin_pi_div_two_sub, sin_add, Orientation.cos_oangle_add_right_of_oangle_eq_pi_div_two, Orientation.cos_oangle_eq_cos_angle, EuclideanGeometry.Sphere.dist_div_cos_oangle_center_eq_two_mul_radius, abs_cos_eq_of_two_zsmul_eq, Orientation.rotation_eq_matrix_toLin, cos_coe, cos_toReal, tan_eq_sin_div_cos, Orientation.cos_oangle_sub_left_mul_norm_of_oangle_eq_pi_div_two, EuclideanGeometry.dist_div_cos_oangle_right_of_oangle_eq_pi_div_two, EuclideanGeometry.dist_div_cos_oangle_left_of_oangle_eq_pi_div_two, cos_pos_iff_abs_toReal_lt_pi_div_two, cos_neg_iff_pi_div_two_lt_abs_toReal, cos_pi_div_two_sub, cos_eq_iff_eq_or_eq_neg, Orientation.rotation_apply, abs_cos_eq_of_two_nsmul_eq, EuclideanGeometry.cos_oangle_right_mul_dist_of_oangle_eq_pi_div_two, cos_neg, cos_sub_pi_div_two, Orientation.cos_oangle_sub_left_of_oangle_eq_pi_div_two, Orientation.norm_div_cos_oangle_sub_right_of_oangle_eq_pi_div_two, cos_antiperiodic, Orientation.rotation_symm_apply, sin_sub_pi_div_two, continuous_cos, EuclideanGeometry.cos_oangle_right_of_oangle_eq_pi_div_two, Orientation.rotationAux_apply, Orientation.cos_oangle_add_left_mul_norm_of_oangle_eq_pi_div_two, Orientation.cos_oangle_eq_inner_div_norm_mul_norm, Orientation.norm_div_cos_oangle_sub_left_of_oangle_eq_pi_div_two, cos_coe_pi
|
instCircularOrder 📖 | CompOp | — |
instCoe 📖 | CompOp | — |
sign 📖 | CompOp | 61 mathmath: EuclideanGeometry.oangle_swap₁₃_sign, Orientation.oangle_sign_smul_add_right, sign_two_zsmul_eq_sign_iff, Orientation.oangle_sign_sub_left_swap, sign_neg_coe_nonpos_of_nonneg_of_le_pi, eq_iff_sign_eq_and_abs_toReal_eq, sign_neg, Wbtw.oangle_sign_eq_of_ne_left, EuclideanGeometry.oangle_sign_eq_zero_iff_collinear, Orientation.oangle_sign_sub_right, EuclideanGeometry.oangle_rotate_sign, continuousAt_sign, Orientation.oangle_sign_sub_smul_left, sign_two_nsmul_eq_neg_sign_iff, sign_pi_sub, Orientation.oangle_sign_sub_smul_right, sign_eq_zero_iff, Sbtw.oangle_sign_eq_right, sign_zero, Sbtw.oangle_sign_eq_of_sbtw, sign_coe_pi, toReal_mem_Ioo_iff_sign_pos, toReal_nonneg_iff_sign_nonneg, sign_sub_pi, Orientation.oangle_sign_neg_left, EuclideanGeometry.oangle_swap₁₂_sign, Sbtw.oangle_sign_eq, Orientation.oangle_sign_smul_left, Orientation.oangle_sign_sub_right_eq_neg, Orientation.oangle_sign_smul_add_smul_smul_add_smul, Orientation.oangle_sign_smul_sub_left, sign_two_nsmul_eq_sign_iff, Collinear.oangle_sign_of_sameRay_vsub, sign_eq_of_continuousOn, Orientation.oangle_sign_sub_left_eq_neg, AffineSubspace.SSameSide.oangle_sign_eq, sign_pi_add, Orientation.oangle_sign_sub_left, sign_two_zsmul_eq_neg_sign_iff, Wbtw.oangle_sign_eq_of_ne_right, Orientation.oangle_sign_smul_right, toReal_neg_iff_sign_neg, Orientation.oangle_sign_add_smul_left, EuclideanGeometry.oangle_swap₂₃_sign, Orientation.oangle_sign_sub_right_swap, ContinuousOn.angle_sign_comp, sign_add_pi, sign_coe_pi_div_two, Orientation.oangle_sign_add_left, Orientation.oangle_sign_neg_right, sign_toReal, sign_coe_nonneg_of_nonneg_of_le_pi, AffineSubspace.SOppSide.oangle_sign_eq_neg, Orientation.oangle_sign_smul_add_smul_right, Sbtw.oangle_sign_eq_left, Orientation.oangle_sign_add_right, Orientation.oangle_sign_smul_add_smul_left, Orientation.oangle_sign_smul_sub_right, sign_coe_neg_pi_div_two, sign_antiperiodic, Sbtw.oangle_sign_eq_of_sbtw_left
|
sin 📖 | CompOp | 57 mathmath: EuclideanGeometry.sin_oangle_right_mul_dist_of_oangle_eq_pi_div_two, EuclideanGeometry.sin_oangle_right_of_oangle_eq_pi_div_two, sin_add_pi_div_two, cos_add, Orientation.sin_oangle_sub_right_mul_norm_of_oangle_eq_pi_div_two, Complex.arg_cos_add_sin_mul_I_coe_angle, sin_eq_zero_iff, Orientation.sin_oangle_add_left_mul_norm_of_oangle_eq_pi_div_two, abs_cos_eq_abs_sin_of_two_zsmul_add_two_zsmul_eq_pi, EuclideanGeometry.Sphere.dist_div_sin_oangle_div_two_eq_radius, cos_sq_add_sin_sq, sin_add_pi, sin_neg, cos_add_pi_div_two, coe_toCircle, Orientation.sin_oangle_add_right_mul_norm_of_oangle_eq_pi_div_two, EuclideanGeometry.Sphere.dist_div_sin_oangle_eq_two_mul_radius, Affine.Triangle.circumsphere_eq_of_dist_of_oangle, Complex.arg_mul_cos_add_sin_mul_I_coe_angle, Orientation.norm_div_sin_oangle_sub_right_of_oangle_eq_pi_div_two, sin_two_nsmul, EuclideanGeometry.dist_div_sin_oangle_left_of_oangle_eq_pi_div_two, Orientation.sin_oangle_add_left_of_oangle_eq_pi_div_two, abs_cos_eq_abs_sin_of_two_nsmul_add_two_nsmul_eq_pi, Orientation.sin_oangle_sub_left_mul_norm_of_oangle_eq_pi_div_two, Affine.Triangle.dist_div_sin_oangle_eq_two_mul_circumradius, Orientation.sin_oangle_sub_left_of_oangle_eq_pi_div_two, sin_coe_pi, sin_pi_div_two_sub, sin_add, Orientation.rotation_eq_matrix_toLin, Orientation.norm_div_sin_oangle_sub_left_of_oangle_eq_pi_div_two, sin_coe, sin_eq_iff_eq_or_add_eq_pi, Orientation.sin_oangle_add_right_of_oangle_eq_pi_div_two, tan_eq_sin_div_cos, Orientation.norm_div_sin_oangle_add_left_of_oangle_eq_pi_div_two, continuous_sin, sin_zero, cos_pi_div_two_sub, EuclideanGeometry.sin_oangle_left_of_oangle_eq_pi_div_two, Orientation.rotation_apply, Orientation.sin_oangle_sub_right_of_oangle_eq_pi_div_two, EuclideanGeometry.sin_oangle_left_mul_dist_of_oangle_eq_pi_div_two, Orientation.norm_div_sin_oangle_add_right_of_oangle_eq_pi_div_two, abs_sin_eq_of_two_zsmul_eq, EuclideanGeometry.dist_div_sin_oangle_right_of_oangle_eq_pi_div_two, cos_sub_pi_div_two, abs_sin_eq_of_two_nsmul_eq, sin_antiperiodic, Affine.Triangle.dist_div_sin_oangle_div_two_eq_circumradius, sin_eq_real_sin_iff_eq_or_add_eq_pi, Orientation.rotation_symm_apply, sin_sub_pi_div_two, sin_toReal, Orientation.rotationAux_apply, sin_sub_pi
|
tan 📖 | CompOp | 36 mathmath: Orientation.tan_oangle_add_left_smul_rotation_pi_div_two, EuclideanGeometry.dist_div_tan_oangle_right_of_oangle_eq_pi_div_two, Orientation.tan_oangle_add_right_smul_rotation_pi_div_two, tan_eq_of_two_nsmul_eq, EuclideanGeometry.tan_oangle_right_of_oangle_eq_pi_div_two, EuclideanGeometry.tan_oangle_left_mul_dist_of_oangle_eq_pi_div_two, Orientation.tan_oangle_sub_right_mul_norm_of_oangle_eq_pi_div_two, EuclideanGeometry.Sphere.tan_div_two_smul_rotation_pi_div_two_vadd_midpoint_eq_center, tan_sub_pi, Orientation.norm_div_tan_oangle_add_left_of_oangle_eq_pi_div_two, Orientation.tan_oangle_add_left_mul_norm_of_oangle_eq_pi_div_two, Affine.Triangle.circumsphere_eq_of_dist_of_oangle, tan_eq_inv_of_two_nsmul_add_two_nsmul_eq_pi, EuclideanGeometry.Sphere.inv_tan_div_two_smul_rotation_pi_div_two_vadd_midpoint_eq_center, Affine.Triangle.inv_tan_div_two_smul_rotation_pi_div_two_vadd_midpoint_eq_circumcenter, Orientation.tan_oangle_sub_left_of_oangle_eq_pi_div_two, EuclideanGeometry.dist_div_tan_oangle_left_of_oangle_eq_pi_div_two, EuclideanGeometry.tan_oangle_right_mul_dist_of_oangle_eq_pi_div_two, Orientation.tan_oangle_sub_left_mul_norm_of_oangle_eq_pi_div_two, tan_eq_sin_div_cos, Orientation.tan_oangle_sub_right_of_oangle_eq_pi_div_two, Orientation.norm_div_tan_oangle_sub_left_of_oangle_eq_pi_div_two, tan_coe_pi, Orientation.tan_oangle_add_left_of_oangle_eq_pi_div_two, Orientation.norm_div_tan_oangle_add_right_of_oangle_eq_pi_div_two, Orientation.tan_oangle_add_right_mul_norm_of_oangle_eq_pi_div_two, tan_add_pi, EuclideanGeometry.tan_oangle_left_of_oangle_eq_pi_div_two, tan_eq_of_two_zsmul_eq, tan_eq_inv_of_two_zsmul_add_two_zsmul_eq_pi, Orientation.norm_div_tan_oangle_sub_right_of_oangle_eq_pi_div_two, Orientation.tan_oangle_add_right_of_oangle_eq_pi_div_two, tan_toReal, tan_periodic, tan_zero, tan_coe
|
toReal 📖 | CompOp | 69 mathmath: abs_toReal_neg_coe_eq_self_iff, sign_two_zsmul_eq_sign_iff, neg_coe_abs_toReal_of_sign_nonpos, toReal_add_of_sign_eq_neg_sign, EuclideanGeometry.abs_oangle_right_toReal_lt_pi_div_two_of_dist_eq, eq_iff_sign_eq_and_abs_toReal_eq, toReal_coe_eq_self_iff_mem_Ioc, abs_toReal_eq_pi_div_two_iff, toReal_eq_pi_iff, abs_toReal_le_pi, toReal_coe, sign_two_nsmul_eq_neg_sign_iff, toReal_pi, toReal_mem_Ioc, toReal_neg_pi_div_two, Complex.arg_coe_angle_eq_iff_eq_toReal, two_nsmul_toReal_eq_two_mul_sub_two_pi, toReal_coe_eq_self_iff, cos_nonneg_iff_abs_toReal_le_pi_div_two, abs_toReal_neg, neg_pi_lt_toReal, coe_abs_toReal_of_sign_nonneg, toReal_neg_eq_neg_toReal_iff, two_zsmul_toReal_eq_two_mul_sub_two_pi, toReal_inj, toReal_mem_Ioo_iff_sign_pos, toReal_nonneg_iff_sign_nonneg, toReal_pi_div_two, toReal_coe_eq_self_sub_two_mul_int_mul_pi_iff, EuclideanGeometry.Sphere.abs_oangle_center_left_toReal_lt_pi_div_two, two_zsmul_toReal_eq_two_mul, EuclideanGeometry.Sphere.abs_oangle_center_right_toReal_lt_pi_div_two, sign_two_nsmul_eq_sign_iff, coe_toReal, toReal_injective, two_nsmul_toReal_eq_two_mul_add_two_pi, sign_two_zsmul_eq_neg_sign_iff, toReal_neg_iff_sign_neg, abs_toReal_add_abs_toReal_eq_pi_of_two_zsmul_add_eq_zero_of_sign_eq, two_zsmul_toReal_eq_two_mul_add_two_pi, toReal_eq_zero_iff, EuclideanGeometry.abs_oangle_left_toReal_lt_pi_div_two_of_dist_eq, cos_toReal, toReal_add_of_sign_pos_sign_neg, abs_toReal_coe_eq_self_iff, toIocMod_toReal, EuclideanGeometry.angle_eq_abs_oangle_toReal, EuclideanGeometry.abs_oangle_toReal_lt_pi_div_two_of_angle_eq_pi_div_two, Orientation.angle_eq_abs_oangle_toReal, cos_pos_iff_abs_toReal_lt_pi_div_two, Complex.arg_coe_angle_toReal_eq_arg, cos_neg_iff_pi_div_two_lt_abs_toReal, sign_toReal, Orientation.abs_oangle_sub_left_toReal_lt_pi_div_two, nsmul_toReal_eq_mul, abs_toReal_add_abs_toReal_eq_pi_of_two_nsmul_add_eq_zero_of_sign_eq, toReal_add_eq_toReal_add_toReal, abs_toReal_add_eq_two_pi_sub_abs_toReal_add_abs_toReal, toReal_le_pi, toReal_coe_eq_self_add_two_pi_iff, toReal_eq_pi_div_two_iff, toReal_coe_eq_self_sub_two_pi_iff, tan_toReal, sin_toReal, toReal_eq_neg_pi_div_two_iff, two_nsmul_toReal_eq_two_mul, Orientation.abs_oangle_sub_right_toReal_lt_pi_div_two, eq_iff_abs_toReal_eq_of_sign_eq, toReal_zero
|