Loogle!

Result

Found 61 declarations mentioning Real.Angle.sin.

• Real.Angle.sin 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
  (θ : Real.Angle) : ℝ
• Real.Angle.sin_coe 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
  (x : ℝ) : (↑x).sin = Real.sin x
• Real.Angle.sin_toReal 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
  (θ : Real.Angle) : Real.sin θ.toReal = θ.sin
• Real.Angle.sin_coe_pi 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
  : (↑Real.pi).sin = 0
• Real.Angle.continuous_sin 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
  : Continuous Real.Angle.sin
• Real.Angle.tan_eq_sin_div_cos 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
  (θ : Real.Angle) : θ.tan = θ.sin / θ.cos
• Real.Angle.tan.eq_1 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
  (θ : Real.Angle) : θ.tan = θ.sin / θ.cos
• Real.Angle.sin_neg 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
  (θ : Real.Angle) : (-θ).sin = -θ.sin
• Real.Angle.sin_sub_pi 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
  (θ : Real.Angle) : (θ - ↑Real.pi).sin = -θ.sin
• Real.Angle.sin_zero 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
  : Real.Angle.sin 0 = 0
• Real.Angle.sin_antiperiodic 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
  : Function.Antiperiodic Real.Angle.sin ↑Real.pi
• Real.Angle.sin_eq_zero_iff 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
  {θ : Real.Angle} : θ.sin = 0 ↔ θ = 0 ∨ θ = ↑Real.pi
• Real.Angle.sin_ne_zero_iff 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
  {θ : Real.Angle} : θ.sin ≠ 0 ↔ θ ≠ 0 ∧ θ ≠ ↑Real.pi
• Real.Angle.cos_pi_div_two_sub 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
  (θ : Real.Angle) : (↑(Real.pi / 2) - θ).cos = θ.sin
• Real.Angle.cos_sub_pi_div_two 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
  (θ : Real.Angle) : (θ - ↑(Real.pi / 2)).cos = θ.sin
• Real.Angle.sin_pi_div_two_sub 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
  (θ : Real.Angle) : (↑(Real.pi / 2) - θ).sin = θ.cos
• Real.Angle.sign.eq_1 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
  (θ : Real.Angle) : θ.sign = SignType.sign θ.sin
• Real.Angle.sin_add_pi 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
  (θ : Real.Angle) : (θ + ↑Real.pi).sin = -θ.sin
• Real.Angle.sin_sub_pi_div_two 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
  (θ : Real.Angle) : (θ - ↑(Real.pi / 2)).sin = -θ.cos
• Real.Angle.cos_sq_add_sin_sq 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
  (θ : Real.Angle) : θ.cos ^ 2 + θ.sin ^ 2 = 1
• Real.Angle.sin_eq_iff_eq_or_add_eq_pi 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
  {θ ψ : Real.Angle} : θ.sin = ψ.sin ↔ θ = ψ ∨ θ + ψ = ↑Real.pi
• Real.Angle.sin_eq_real_sin_iff_eq_or_add_eq_pi 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
  {θ : Real.Angle} {ψ : ℝ} : θ.sin = Real.sin ψ ↔ θ = ↑ψ ∨ θ + ↑ψ = ↑Real.pi
• Real.Angle.abs_sin_eq_of_two_zsmul_eq 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
  {θ ψ : Real.Angle} (h : 2 • θ = 2 • ψ) : |θ.sin| = |ψ.sin|
• Real.Angle.sin_add_pi_div_two 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
  (θ : Real.Angle) : (θ + ↑(Real.pi / 2)).sin = θ.cos
• Real.Angle.cos_add_pi_div_two 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
  (θ : Real.Angle) : (θ + ↑(Real.pi / 2)).cos = -θ.sin
• Real.Angle.cos_add 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
  (θ₁ θ₂ : Real.Angle) : (θ₁ + θ₂).cos = θ₁.cos * θ₂.cos - θ₁.sin * θ₂.sin
• Real.Angle.sin_add 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
  (θ₁ θ₂ : Real.Angle) : (θ₁ + θ₂).sin = θ₁.sin * θ₂.cos + θ₁.cos * θ₂.sin
• Real.Angle.abs_cos_eq_abs_sin_of_two_zsmul_add_two_zsmul_eq_pi 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
  {θ ψ : Real.Angle} (h : 2 • θ + 2 • ψ = ↑Real.pi) : |θ.cos| = |ψ.sin|
• Real.Angle.abs_sin_eq_of_two_nsmul_eq 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
  {θ ψ : Real.Angle} (h : 2 • θ = 2 • ψ) : |θ.sin| = |ψ.sin|
• Real.Angle.abs_cos_eq_abs_sin_of_two_nsmul_add_two_nsmul_eq_pi 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
  {θ ψ : Real.Angle} (h : 2 • θ + 2 • ψ = ↑Real.pi) : |θ.cos| = |ψ.sin|
• Complex.arg_cos_add_sin_mul_I_coe_angle 📋 Mathlib.Analysis.SpecialFunctions.Complex.Arg
  (θ : Real.Angle) : ↑(↑θ.cos + ↑θ.sin * Complex.I).arg = θ
• Complex.arg_mul_cos_add_sin_mul_I_coe_angle 📋 Mathlib.Analysis.SpecialFunctions.Complex.Arg
  {r : ℝ} (hr : 0 < r) (θ : Real.Angle) : ↑(↑r * (↑θ.cos + ↑θ.sin * Complex.I)).arg = θ
• Real.Angle.coe_toCircle 📋 Mathlib.Analysis.SpecialFunctions.Complex.Circle
  (θ : Real.Angle) : ↑θ.toCircle = ↑θ.cos + ↑θ.sin * Complex.I
• Orientation.rotationAux_apply 📋 Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
  {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (Module.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (θ : Real.Angle) (x : V) : (o.rotationAux θ) x = θ.cos • x + θ.sin • o.rightAngleRotation x
• Orientation.rotation_apply 📋 Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
  {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (Module.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (θ : Real.Angle) (x : V) : (o.rotation θ) x = θ.cos • x + θ.sin • o.rightAngleRotation x
• Orientation.rotation_symm_apply 📋 Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
  {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (Module.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (θ : Real.Angle) (x : V) : (o.rotation θ).symm x = θ.cos • x - θ.sin • o.rightAngleRotation x
• Orientation.rotation.eq_1 📋 Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
  {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (Module.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (θ : Real.Angle) : o.rotation θ = LinearIsometryEquiv.ofLinearIsometry (o.rotationAux θ) (θ.cos • LinearMap.id - θ.sin • ↑o.rightAngleRotation.toLinearEquiv) ⋯ ⋯
• Orientation.rotation_eq_matrix_toLin 📋 Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
  {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (Module.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (θ : Real.Angle) {x : V} (hx : x ≠ 0) : ↑(o.rotation θ).toLinearEquiv = (Matrix.toLin (o.basisRightAngleRotation x hx) (o.basisRightAngleRotation x hx)) !![θ.cos, -θ.sin; θ.sin, θ.cos]
• EuclideanGeometry.sin_oangle_left_mul_dist_of_oangle_eq_pi_div_two 📋 Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
  {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ : P} (h : EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(Real.pi / 2)) : (EuclideanGeometry.oangle p₃ p₁ p₂).sin * dist p₁ p₃ = dist p₃ p₂
• EuclideanGeometry.sin_oangle_right_mul_dist_of_oangle_eq_pi_div_two 📋 Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
  {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ : P} (h : EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(Real.pi / 2)) : (EuclideanGeometry.oangle p₂ p₃ p₁).sin * dist p₁ p₃ = dist p₁ p₂
• EuclideanGeometry.dist_div_sin_oangle_left_of_oangle_eq_pi_div_two 📋 Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
  {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ : P} (h : EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(Real.pi / 2)) : dist p₃ p₂ / (EuclideanGeometry.oangle p₃ p₁ p₂).sin = dist p₁ p₃
• EuclideanGeometry.dist_div_sin_oangle_right_of_oangle_eq_pi_div_two 📋 Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
  {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ : P} (h : EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(Real.pi / 2)) : dist p₁ p₂ / (EuclideanGeometry.oangle p₂ p₃ p₁).sin = dist p₁ p₃
• EuclideanGeometry.sin_oangle_left_of_oangle_eq_pi_div_two 📋 Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
  {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ : P} (h : EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(Real.pi / 2)) : (EuclideanGeometry.oangle p₃ p₁ p₂).sin = dist p₃ p₂ / dist p₁ p₃
• EuclideanGeometry.sin_oangle_right_of_oangle_eq_pi_div_two 📋 Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
  {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ : P} (h : EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(Real.pi / 2)) : (EuclideanGeometry.oangle p₂ p₃ p₁).sin = dist p₁ p₂ / dist p₁ p₃
• Orientation.sin_oangle_sub_left_mul_norm_of_oangle_eq_pi_div_two 📋 Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
  {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [hd2 : Fact (Module.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V} (h : o.oangle x y = ↑(Real.pi / 2)) : (o.oangle (x - y) x).sin * ‖x - y‖ = ‖y‖
• Orientation.sin_oangle_sub_right_mul_norm_of_oangle_eq_pi_div_two 📋 Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
  {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [hd2 : Fact (Module.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V} (h : o.oangle x y = ↑(Real.pi / 2)) : (o.oangle y (y - x)).sin * ‖y - x‖ = ‖x‖
• Orientation.norm_div_sin_oangle_sub_left_of_oangle_eq_pi_div_two 📋 Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
  {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [hd2 : Fact (Module.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V} (h : o.oangle x y = ↑(Real.pi / 2)) : ‖y‖ / (o.oangle (x - y) x).sin = ‖x - y‖
• Orientation.norm_div_sin_oangle_sub_right_of_oangle_eq_pi_div_two 📋 Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
  {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [hd2 : Fact (Module.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V} (h : o.oangle x y = ↑(Real.pi / 2)) : ‖x‖ / (o.oangle y (y - x)).sin = ‖y - x‖
• Orientation.sin_oangle_sub_left_of_oangle_eq_pi_div_two 📋 Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
  {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [hd2 : Fact (Module.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V} (h : o.oangle x y = ↑(Real.pi / 2)) : (o.oangle (x - y) x).sin = ‖y‖ / ‖x - y‖
• Orientation.sin_oangle_sub_right_of_oangle_eq_pi_div_two 📋 Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
  {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [hd2 : Fact (Module.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V} (h : o.oangle x y = ↑(Real.pi / 2)) : (o.oangle y (y - x)).sin = ‖x‖ / ‖y - x‖
• Orientation.sin_oangle_add_left_mul_norm_of_oangle_eq_pi_div_two 📋 Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
  {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [hd2 : Fact (Module.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V} (h : o.oangle x y = ↑(Real.pi / 2)) : (o.oangle (x + y) y).sin * ‖x + y‖ = ‖x‖
• Orientation.sin_oangle_add_right_mul_norm_of_oangle_eq_pi_div_two 📋 Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
  {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [hd2 : Fact (Module.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V} (h : o.oangle x y = ↑(Real.pi / 2)) : (o.oangle x (x + y)).sin * ‖x + y‖ = ‖y‖
• Orientation.norm_div_sin_oangle_add_left_of_oangle_eq_pi_div_two 📋 Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
  {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [hd2 : Fact (Module.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V} (h : o.oangle x y = ↑(Real.pi / 2)) : ‖x‖ / (o.oangle (x + y) y).sin = ‖x + y‖
• Orientation.norm_div_sin_oangle_add_right_of_oangle_eq_pi_div_two 📋 Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
  {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [hd2 : Fact (Module.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V} (h : o.oangle x y = ↑(Real.pi / 2)) : ‖y‖ / (o.oangle x (x + y)).sin = ‖x + y‖
• Orientation.sin_oangle_add_left_of_oangle_eq_pi_div_two 📋 Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
  {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [hd2 : Fact (Module.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V} (h : o.oangle x y = ↑(Real.pi / 2)) : (o.oangle (x + y) y).sin = ‖x‖ / ‖x + y‖
• Orientation.sin_oangle_add_right_of_oangle_eq_pi_div_two 📋 Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
  {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [hd2 : Fact (Module.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V} (h : o.oangle x y = ↑(Real.pi / 2)) : (o.oangle x (x + y)).sin = ‖y‖ / ‖x + y‖
• EuclideanGeometry.Sphere.dist_div_sin_oangle_eq_two_mul_radius 📋 Mathlib.Geometry.Euclidean.Angle.Sphere
  {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {s : EuclideanGeometry.Sphere P} {p₁ p₂ p₃ : P} (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) (hp₃ : p₃ ∈ s) (hp₁p₂ : p₁ ≠ p₂) (hp₁p₃ : p₁ ≠ p₃) (hp₂p₃ : p₂ ≠ p₃) : dist p₁ p₃ / |(EuclideanGeometry.oangle p₁ p₂ p₃).sin| = 2 * s.radius
• EuclideanGeometry.Sphere.dist_div_sin_oangle_div_two_eq_radius 📋 Mathlib.Geometry.Euclidean.Angle.Sphere
  {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {s : EuclideanGeometry.Sphere P} {p₁ p₂ p₃ : P} (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) (hp₃ : p₃ ∈ s) (hp₁p₂ : p₁ ≠ p₂) (hp₁p₃ : p₁ ≠ p₃) (hp₂p₃ : p₂ ≠ p₃) : dist p₁ p₃ / |(EuclideanGeometry.oangle p₁ p₂ p₃).sin| / 2 = s.radius
• Affine.Triangle.dist_div_sin_oangle_eq_two_mul_circumradius 📋 Mathlib.Geometry.Euclidean.Angle.Sphere
  {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] (t : Affine.Triangle ℝ P) {i₁ i₂ i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) : dist (t.points i₁) (t.points i₃) / |(EuclideanGeometry.oangle (t.points i₁) (t.points i₂) (t.points i₃)).sin| = 2 * Affine.Simplex.circumradius t
• Affine.Triangle.dist_div_sin_oangle_div_two_eq_circumradius 📋 Mathlib.Geometry.Euclidean.Angle.Sphere
  {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] (t : Affine.Triangle ℝ P) {i₁ i₂ i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) : dist (t.points i₁) (t.points i₃) / |(EuclideanGeometry.oangle (t.points i₁) (t.points i₂) (t.points i₃)).sin| / 2 = Affine.Simplex.circumradius t
• Affine.Triangle.circumsphere_eq_of_dist_of_oangle 📋 Mathlib.Geometry.Euclidean.Angle.Sphere
  {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] (t : Affine.Triangle ℝ P) {i₁ i₂ i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) : Affine.Simplex.circumsphere t = { center := ((EuclideanGeometry.oangle (t.points i₁) (t.points i₂) (t.points i₃)).tan⁻¹ / 2) • (EuclideanGeometry.o.rotation ↑(Real.pi / 2)) (t.points i₃ -ᵥ t.points i₁) +ᵥ midpoint ℝ (t.points i₁) (t.points i₃), radius := dist (t.points i₁) (t.points i₃) / |(EuclideanGeometry.oangle (t.points i₁) (t.points i₂) (t.points i₃)).sin| / 2 }

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using (by default) Ctrl-K Ctrl-S. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO.

This is Loogle revision 06e7f72 serving mathlib revision e128198