Documentation

EuclideanGeometry.Foundation.Axiom.Basic.Angle.FromMathlib

APIs about Angle from Mathlib #

We use AngValue as an alias of Real.Angle.

source
def EuclidGeom.AngValue :
Type
Equations
Instances For
    source
    instance EuclidGeom.AngValue.instNormedAddCommGroupAngValue :
    NormedAddCommGroup EuclidGeom.AngValue
    Equations
    source
    instance EuclidGeom.AngValue.instInhabitedAngValue :
    Inhabited EuclidGeom.AngValue
    Equations
    source
    def EuclidGeom.AngValue.coe (r : ℝ) :
    EuclidGeom.AngValue

    The canonical map from ℝ to the quotient AngValue.

    Equations
    • ↑r = ↑r
    Instances For
      source
      instance EuclidGeom.AngValue.instCoeRealAngValue :
      Coe ℝ EuclidGeom.AngValue
      Equations
      source
      instance EuclidGeom.AngValue.instCircularOrderAngValue :
      CircularOrder EuclidGeom.AngValue
      Equations
      source
      theorem EuclidGeom.AngValue.continuous_coe :
      Continuous EuclidGeom.AngValue.coe
      source
      def EuclidGeom.AngValue.coeHom :
      ℝ →+ EuclidGeom.AngValue

      Coercion ℝ → AngValue as an additive homomorphism.

      Equations
      Instances For
        source
        @[simp]
        theorem EuclidGeom.AngValue.coe_coeHom :
        ⇑EuclidGeom.AngValue.coeHom = EuclidGeom.AngValue.coe
        source
        theorem EuclidGeom.AngValue.induction_on {p : EuclidGeom.AngValue → Prop} (θ : EuclidGeom.AngValue) (h : ∀ (x : ℝ), p ↑x) :
        p θ

        An induction principle to deduce results for AngValue from those for ℝ, used with induction θ using AngValue.induction_on.

        source
        @[simp]
        theorem EuclidGeom.AngValue.coe_zero :
        ↑0 = 0
        source
        @[simp]
        theorem EuclidGeom.AngValue.coe_add (x : ℝ) (y : ℝ) :
        ↑(x + y) = ↑x + ↑y
        source
        @[simp]
        theorem EuclidGeom.AngValue.coe_neg (x : ℝ) :
        ↑(-x) = -↑x
        source
        @[simp]
        theorem EuclidGeom.AngValue.coe_sub (x : ℝ) (y : ℝ) :
        ↑(x - y) = ↑x - ↑y
        source
        theorem EuclidGeom.AngValue.coe_nsmul (n : ℕ) (x : ℝ) :
        ↑(n • x) = n • ↑x
        source
        theorem EuclidGeom.AngValue.coe_zsmul (z : ℤ) (x : ℝ) :
        ↑(z • x) = z • ↑x
        source
        @[simp]
        theorem EuclidGeom.AngValue.coe_nat_mul_eq_nsmul (x : ℝ) (n : ℕ) :
        ↑(↑n * x) = n • ↑x
        source
        @[simp]
        theorem EuclidGeom.AngValue.coe_int_mul_eq_zsmul (x : ℝ) (n : ℤ) :
        ↑(↑n * x) = n • ↑x
        source
        theorem EuclidGeom.AngValue.eq_iff_two_pi_dvd_sub {ψ : ℝ} {θ : ℝ} :
        ↑θ = ↑ψ ↔ ∃ (k : ℤ), θ - ψ = 2 * Real.pi * ↑k
        source
        @[simp]
        theorem EuclidGeom.AngValue.coe_two_pi :
        ↑(2 * Real.pi) = 0
        source
        @[simp]
        theorem EuclidGeom.AngValue.neg_coe_pi :
        -↑Real.pi = ↑Real.pi
        source
        @[simp]
        theorem EuclidGeom.AngValue.two_nsmul_coe_div_two (θ : ℝ) :
        2 • ↑(θ / 2) = ↑θ
        source
        @[simp]
        theorem EuclidGeom.AngValue.two_zsmul_coe_div_two (θ : ℝ) :
        2 • ↑(θ / 2) = ↑θ
        source
        theorem EuclidGeom.AngValue.two_nsmul_neg_pi_div_two :
        2 • ↑(-Real.pi / 2) = ↑Real.pi
        source
        theorem EuclidGeom.AngValue.two_zsmul_neg_pi_div_two :
        2 • ↑(-Real.pi / 2) = ↑Real.pi
        source
        theorem EuclidGeom.AngValue.sub_coe_pi_eq_add_coe_pi (θ : EuclidGeom.AngValue) :
        θ - ↑Real.pi = θ + ↑Real.pi
        source
        @[simp]
        theorem EuclidGeom.AngValue.two_nsmul_coe_pi :
        2 • ↑Real.pi = 0
        source
        @[simp]
        theorem EuclidGeom.AngValue.two_zsmul_coe_pi :
        2 • ↑Real.pi = 0
        source
        @[simp]
        theorem EuclidGeom.AngValue.coe_pi_add_coe_pi :
        ↑Real.pi + ↑Real.pi = 0
        source
        theorem EuclidGeom.AngValue.zsmul_eq_iff {ψ : EuclidGeom.AngValue} {θ : EuclidGeom.AngValue} {z : ℤ} (hz : z ≠ 0) :
        z • ψ = z • θ ↔ ∃ (k : Fin (Int.natAbs z)), ψ = θ + ↑k • ↑(2 * Real.pi / ↑z)
        source
        theorem EuclidGeom.AngValue.nsmul_eq_iff {ψ : EuclidGeom.AngValue} {θ : EuclidGeom.AngValue} {n : ℕ} (hz : n ≠ 0) :
        n • ψ = n • θ ↔ ∃ (k : Fin n), ψ = θ + ↑k • ↑(2 * Real.pi / ↑n)
        source
        theorem EuclidGeom.AngValue.two_zsmul_eq_iff {ψ : EuclidGeom.AngValue} {θ : EuclidGeom.AngValue} :
        2 • ψ = 2 • θ ↔ ψ = θ ∨ ψ = θ + ↑Real.pi
        source
        theorem EuclidGeom.AngValue.two_nsmul_eq_iff {ψ : EuclidGeom.AngValue} {θ : EuclidGeom.AngValue} :
        2 • ψ = 2 • θ ↔ ψ = θ ∨ ψ = θ + ↑Real.pi
        source
        theorem EuclidGeom.AngValue.two_nsmul_eq_zero_iff {θ : EuclidGeom.AngValue} :
        2 • θ = 0 ↔ θ = 0 ∨ θ = ↑Real.pi
        source
        theorem EuclidGeom.AngValue.two_nsmul_ne_zero_iff {θ : EuclidGeom.AngValue} :
        2 • θ ≠ 0 ↔ θ ≠ 0 ∧ θ ≠ ↑Real.pi
        source
        theorem EuclidGeom.AngValue.two_zsmul_eq_zero_iff {θ : EuclidGeom.AngValue} :
        2 • θ = 0 ↔ θ = 0 ∨ θ = ↑Real.pi
        source
        theorem EuclidGeom.AngValue.two_zsmul_ne_zero_iff {θ : EuclidGeom.AngValue} :
        2 • θ ≠ 0 ↔ θ ≠ 0 ∧ θ ≠ ↑Real.pi
        source
        theorem EuclidGeom.AngValue.eq_neg_self_iff {θ : EuclidGeom.AngValue} :
        θ = -θ ↔ θ = 0 ∨ θ = ↑Real.pi
        source
        theorem EuclidGeom.AngValue.ne_neg_self_iff {θ : EuclidGeom.AngValue} :
        θ ≠ -θ ↔ θ ≠ 0 ∧ θ ≠ ↑Real.pi
        source
        theorem EuclidGeom.AngValue.neg_eq_self_iff {θ : EuclidGeom.AngValue} :
        -θ = θ ↔ θ = 0 ∨ θ = ↑Real.pi
        source
        theorem EuclidGeom.AngValue.neg_ne_self_iff {θ : EuclidGeom.AngValue} :
        -θ ≠ θ ↔ θ ≠ 0 ∧ θ ≠ ↑Real.pi
        source
        theorem EuclidGeom.AngValue.two_nsmul_eq_pi_iff {θ : EuclidGeom.AngValue} :
        2 • θ = ↑Real.pi ↔ θ = ↑(Real.pi / 2) ∨ θ = ↑(-Real.pi / 2)
        source
        theorem EuclidGeom.AngValue.two_zsmul_eq_pi_iff {θ : EuclidGeom.AngValue} :
        2 • θ = ↑Real.pi ↔ θ = ↑(Real.pi / 2) ∨ θ = ↑(-Real.pi / 2)
        source
        theorem EuclidGeom.AngValue.cos_eq_iff_coe_eq_or_eq_neg {θ : ℝ} {ψ : ℝ} :
        Real.cos θ = Real.cos ψ ↔ ↑θ = ↑ψ ∨ ↑θ = -↑ψ
        source
        theorem EuclidGeom.AngValue.sin_eq_iff_coe_eq_or_add_eq_pi {θ : ℝ} {ψ : ℝ} :
        Real.sin θ = Real.sin ψ ↔ ↑θ = ↑ψ ∨ ↑θ + ↑ψ = ↑Real.pi
        source
        theorem EuclidGeom.AngValue.cos_sin_inj {θ : ℝ} {ψ : ℝ} (Hcos : Real.cos θ = Real.cos ψ) (Hsin : Real.sin θ = Real.sin ψ) :
        ↑θ = ↑ψ
        source
        def EuclidGeom.AngValue.sin (θ : EuclidGeom.AngValue) :
        ℝ

        The sine of a AngValue.

        Equations
        Instances For
          source
          @[simp]
          theorem EuclidGeom.AngValue.sin_coe (x : ℝ) :
          EuclidGeom.AngValue.sin ↑x = Real.sin x
          source
          theorem EuclidGeom.AngValue.continuous_sin :
          Continuous EuclidGeom.AngValue.sin
          source
          def EuclidGeom.AngValue.cos (θ : EuclidGeom.AngValue) :
          ℝ

          The cosine of a AngValue.

          Equations
          Instances For
            source
            @[simp]
            theorem EuclidGeom.AngValue.cos_coe (x : ℝ) :
            EuclidGeom.AngValue.cos ↑x = Real.cos x
            source
            theorem EuclidGeom.AngValue.continuous_cos :
            Continuous EuclidGeom.AngValue.cos
            source
            theorem EuclidGeom.AngValue.cos_eq_real_cos_iff_eq_or_eq_neg {θ : EuclidGeom.AngValue} {ψ : ℝ} :
            EuclidGeom.AngValue.cos θ = Real.cos ψ ↔ θ = ↑ψ ∨ θ = -↑ψ
            source
            theorem EuclidGeom.AngValue.cos_eq_iff_eq_or_eq_neg {θ : EuclidGeom.AngValue} {ψ : EuclidGeom.AngValue} :
            EuclidGeom.AngValue.cos θ = EuclidGeom.AngValue.cos ψ ↔ θ = ψ ∨ θ = -ψ
            source
            theorem EuclidGeom.AngValue.sin_eq_real_sin_iff_eq_or_add_eq_pi {θ : EuclidGeom.AngValue} {ψ : ℝ} :
            EuclidGeom.AngValue.sin θ = Real.sin ψ ↔ θ = ↑ψ ∨ θ + ↑ψ = ↑Real.pi
            source
            theorem EuclidGeom.AngValue.sin_eq_iff_eq_or_add_eq_pi {θ : EuclidGeom.AngValue} {ψ : EuclidGeom.AngValue} :
            EuclidGeom.AngValue.sin θ = EuclidGeom.AngValue.sin ψ ↔ θ = ψ ∨ θ + ψ = ↑Real.pi
            source
            @[simp]
            theorem EuclidGeom.AngValue.sin_zero :
            EuclidGeom.AngValue.sin 0 = 0
            source
            theorem EuclidGeom.AngValue.sin_coe_pi :
            EuclidGeom.AngValue.sin ↑Real.pi = 0
            source
            theorem EuclidGeom.AngValue.sin_eq_zero_iff {θ : EuclidGeom.AngValue} :
            EuclidGeom.AngValue.sin θ = 0 ↔ θ = 0 ∨ θ = ↑Real.pi
            source
            theorem EuclidGeom.AngValue.sin_ne_zero_iff {θ : EuclidGeom.AngValue} :
            EuclidGeom.AngValue.sin θ ≠ 0 ↔ θ ≠ 0 ∧ θ ≠ ↑Real.pi
            source
            @[simp]
            theorem EuclidGeom.AngValue.sin_neg (θ : EuclidGeom.AngValue) :
            EuclidGeom.AngValue.sin (-θ) = -EuclidGeom.AngValue.sin θ
            source
            theorem EuclidGeom.AngValue.sin_antiperiodic :
            Function.Antiperiodic EuclidGeom.AngValue.sin ↑Real.pi
            source
            @[simp]
            theorem EuclidGeom.AngValue.sin_add_pi (θ : EuclidGeom.AngValue) :
            EuclidGeom.AngValue.sin (θ + ↑Real.pi) = -EuclidGeom.AngValue.sin θ
            source
            @[simp]
            theorem EuclidGeom.AngValue.sin_sub_pi (θ : EuclidGeom.AngValue) :
            EuclidGeom.AngValue.sin (θ - ↑Real.pi) = -EuclidGeom.AngValue.sin θ
            source
            @[simp]
            theorem EuclidGeom.AngValue.cos_zero :
            EuclidGeom.AngValue.cos 0 = 1
            source
            theorem EuclidGeom.AngValue.cos_coe_pi :
            EuclidGeom.AngValue.cos ↑Real.pi = -1
            source
            @[simp]
            theorem EuclidGeom.AngValue.cos_neg (θ : EuclidGeom.AngValue) :
            EuclidGeom.AngValue.cos (-θ) = EuclidGeom.AngValue.cos θ
            source
            theorem EuclidGeom.AngValue.cos_antiperiodic :
            Function.Antiperiodic EuclidGeom.AngValue.cos ↑Real.pi
            source
            @[simp]
            theorem EuclidGeom.AngValue.cos_add_pi (θ : EuclidGeom.AngValue) :
            EuclidGeom.AngValue.cos (θ + ↑Real.pi) = -EuclidGeom.AngValue.cos θ
            source
            @[simp]
            theorem EuclidGeom.AngValue.cos_sub_pi (θ : EuclidGeom.AngValue) :
            EuclidGeom.AngValue.cos (θ - ↑Real.pi) = -EuclidGeom.AngValue.cos θ
            source
            theorem EuclidGeom.AngValue.cos_eq_zero_iff {θ : EuclidGeom.AngValue} :
            EuclidGeom.AngValue.cos θ = 0 ↔ θ = ↑(Real.pi / 2) ∨ θ = ↑(-Real.pi / 2)
            source
            theorem EuclidGeom.AngValue.sin_add (θ₁ : EuclidGeom.AngValue) (θ₂ : EuclidGeom.AngValue) :
            EuclidGeom.AngValue.sin (θ₁ + θ₂) = EuclidGeom.AngValue.sin θ₁ * EuclidGeom.AngValue.cos θ₂ + EuclidGeom.AngValue.cos θ₁ * EuclidGeom.AngValue.sin θ₂
            source
            theorem EuclidGeom.AngValue.cos_add (θ₁ : EuclidGeom.AngValue) (θ₂ : EuclidGeom.AngValue) :
            EuclidGeom.AngValue.cos (θ₁ + θ₂) = EuclidGeom.AngValue.cos θ₁ * EuclidGeom.AngValue.cos θ₂ - EuclidGeom.AngValue.sin θ₁ * EuclidGeom.AngValue.sin θ₂
            source
            @[simp]
            theorem EuclidGeom.AngValue.cos_sq_add_sin_sq (θ : EuclidGeom.AngValue) :
            EuclidGeom.AngValue.cos θ ^ 2 + EuclidGeom.AngValue.sin θ ^ 2 = 1
            source
            @[simp]
            theorem EuclidGeom.AngValue.sin_add_pi_div_two (θ : EuclidGeom.AngValue) :
            EuclidGeom.AngValue.sin (θ + ↑(Real.pi / 2)) = EuclidGeom.AngValue.cos θ
            source
            @[simp]
            theorem EuclidGeom.AngValue.sin_sub_pi_div_two (θ : EuclidGeom.AngValue) :
            EuclidGeom.AngValue.sin (θ - ↑(Real.pi / 2)) = -EuclidGeom.AngValue.cos θ
            source
            @[simp]
            theorem EuclidGeom.AngValue.sin_pi_div_two_sub (θ : EuclidGeom.AngValue) :
            EuclidGeom.AngValue.sin (↑(Real.pi / 2) - θ) = EuclidGeom.AngValue.cos θ
            source
            @[simp]
            theorem EuclidGeom.AngValue.cos_add_pi_div_two (θ : EuclidGeom.AngValue) :
            EuclidGeom.AngValue.cos (θ + ↑(Real.pi / 2)) = -EuclidGeom.AngValue.sin θ
            source
            @[simp]
            theorem EuclidGeom.AngValue.cos_sub_pi_div_two (θ : EuclidGeom.AngValue) :
            EuclidGeom.AngValue.cos (θ - ↑(Real.pi / 2)) = EuclidGeom.AngValue.sin θ
            source
            @[simp]
            theorem EuclidGeom.AngValue.cos_pi_div_two_sub (θ : EuclidGeom.AngValue) :
            EuclidGeom.AngValue.cos (↑(Real.pi / 2) - θ) = EuclidGeom.AngValue.sin θ
            source
            theorem EuclidGeom.AngValue.abs_sin_eq_of_two_nsmul_eq {θ : EuclidGeom.AngValue} {ψ : EuclidGeom.AngValue} (h : 2 • θ = 2 • ψ) :
            |EuclidGeom.AngValue.sin θ| = |EuclidGeom.AngValue.sin ψ|
            source
            theorem EuclidGeom.AngValue.abs_sin_eq_of_two_zsmul_eq {θ : EuclidGeom.AngValue} {ψ : EuclidGeom.AngValue} (h : 2 • θ = 2 • ψ) :
            |EuclidGeom.AngValue.sin θ| = |EuclidGeom.AngValue.sin ψ|
            source
            theorem EuclidGeom.AngValue.abs_cos_eq_of_two_nsmul_eq {θ : EuclidGeom.AngValue} {ψ : EuclidGeom.AngValue} (h : 2 • θ = 2 • ψ) :
            |EuclidGeom.AngValue.cos θ| = |EuclidGeom.AngValue.cos ψ|
            source
            theorem EuclidGeom.AngValue.abs_cos_eq_of_two_zsmul_eq {θ : EuclidGeom.AngValue} {ψ : EuclidGeom.AngValue} (h : 2 • θ = 2 • ψ) :
            |EuclidGeom.AngValue.cos θ| = |EuclidGeom.AngValue.cos ψ|
            source
            @[simp]
            theorem EuclidGeom.AngValue.coe_toIcoMod (θ : ℝ) (ψ : ℝ) :
            ↑(toIcoMod Real.two_pi_pos ψ θ) = ↑θ
            source
            @[simp]
            theorem EuclidGeom.AngValue.coe_toIocMod (θ : ℝ) (ψ : ℝ) :
            ↑(toIocMod Real.two_pi_pos ψ θ) = ↑θ
            source
            def EuclidGeom.AngValue.toReal (θ : EuclidGeom.AngValue) :
            ℝ

            Convert a AngValue to a real number in the interval Ioc (-π) π.

            Equations
            Instances For
              source
              theorem EuclidGeom.AngValue.toReal_coe (θ : ℝ) :
              EuclidGeom.AngValue.toReal ↑θ = toIocMod Real.two_pi_pos (-Real.pi) θ
              source
              theorem EuclidGeom.AngValue.toReal_coe_eq_self_iff {θ : ℝ} :
              EuclidGeom.AngValue.toReal ↑θ = θ ↔ -Real.pi < θ ∧ θ ≤ Real.pi
              source
              theorem EuclidGeom.AngValue.toReal_coe_eq_self_iff_mem_Ioc {θ : ℝ} :
              EuclidGeom.AngValue.toReal ↑θ = θ ↔ θ ∈ Set.Ioc (-Real.pi) Real.pi
              source
              theorem EuclidGeom.AngValue.toReal_injective :
              Function.Injective EuclidGeom.AngValue.toReal
              source
              @[simp]
              theorem EuclidGeom.AngValue.toReal_inj {θ : EuclidGeom.AngValue} {ψ : EuclidGeom.AngValue} :
              EuclidGeom.AngValue.toReal θ = EuclidGeom.AngValue.toReal ψ ↔ θ = ψ
              source
              @[simp]
              theorem EuclidGeom.AngValue.coe_toReal (θ : EuclidGeom.AngValue) :
              ↑(EuclidGeom.AngValue.toReal θ) = θ
              source
              theorem EuclidGeom.AngValue.neg_pi_lt_toReal (θ : EuclidGeom.AngValue) :
              -Real.pi < EuclidGeom.AngValue.toReal θ
              source
              theorem EuclidGeom.AngValue.toReal_le_pi (θ : EuclidGeom.AngValue) :
              EuclidGeom.AngValue.toReal θ ≤ Real.pi
              source
              theorem EuclidGeom.AngValue.abs_toReal_le_pi (θ : EuclidGeom.AngValue) :
              |EuclidGeom.AngValue.toReal θ| ≤ Real.pi
              source
              theorem EuclidGeom.AngValue.toReal_mem_Ioc (θ : EuclidGeom.AngValue) :
              EuclidGeom.AngValue.toReal θ ∈ Set.Ioc (-Real.pi) Real.pi
              source
              @[simp]
              theorem EuclidGeom.AngValue.toIocMod_toReal (θ : EuclidGeom.AngValue) :
              toIocMod Real.two_pi_pos (-Real.pi) (EuclidGeom.AngValue.toReal θ) = EuclidGeom.AngValue.toReal θ
              source
              @[simp]
              theorem EuclidGeom.AngValue.toReal_zero :
              EuclidGeom.AngValue.toReal 0 = 0
              source
              @[simp]
              theorem EuclidGeom.AngValue.toReal_eq_zero_iff {θ : EuclidGeom.AngValue} :
              EuclidGeom.AngValue.toReal θ = 0 ↔ θ = 0
              source
              @[simp]
              theorem EuclidGeom.AngValue.toReal_pi :
              EuclidGeom.AngValue.toReal ↑Real.pi = Real.pi
              source
              @[simp]
              theorem EuclidGeom.AngValue.toReal_eq_pi_iff {θ : EuclidGeom.AngValue} :
              EuclidGeom.AngValue.toReal θ = Real.pi ↔ θ = ↑Real.pi
              source
              theorem EuclidGeom.AngValue.pi_ne_zero :
              ↑Real.pi ≠ 0
              source
              @[simp]
              theorem EuclidGeom.AngValue.toReal_pi_div_two :
              EuclidGeom.AngValue.toReal ↑(Real.pi / 2) = Real.pi / 2
              source
              @[simp]
              theorem EuclidGeom.AngValue.toReal_eq_pi_div_two_iff {θ : EuclidGeom.AngValue} :
              EuclidGeom.AngValue.toReal θ = Real.pi / 2 ↔ θ = ↑(Real.pi / 2)
              source
              @[simp]
              theorem EuclidGeom.AngValue.toReal_neg_pi_div_two :
              EuclidGeom.AngValue.toReal ↑(-Real.pi / 2) = -Real.pi / 2
              source
              @[simp]
              theorem EuclidGeom.AngValue.toReal_eq_neg_pi_div_two_iff {θ : EuclidGeom.AngValue} :
              EuclidGeom.AngValue.toReal θ = -Real.pi / 2 ↔ θ = ↑(-Real.pi / 2)
              source
              theorem EuclidGeom.AngValue.pi_div_two_ne_zero :
              ↑(Real.pi / 2) ≠ 0
              source
              theorem EuclidGeom.AngValue.neg_pi_div_two_ne_zero :
              ↑(-Real.pi / 2) ≠ 0
              source
              theorem EuclidGeom.AngValue.abs_toReal_coe_eq_self_iff {θ : ℝ} :
              |EuclidGeom.AngValue.toReal ↑θ| = θ ↔ 0 ≤ θ ∧ θ ≤ Real.pi
              source
              theorem EuclidGeom.AngValue.abs_toReal_neg_coe_eq_self_iff {θ : ℝ} :
              |EuclidGeom.AngValue.toReal (-↑θ)| = θ ↔ 0 ≤ θ ∧ θ ≤ Real.pi
              source
              theorem EuclidGeom.AngValue.abs_toReal_eq_pi_div_two_iff {θ : EuclidGeom.AngValue} :
              |EuclidGeom.AngValue.toReal θ| = Real.pi / 2 ↔ θ = ↑(Real.pi / 2) ∨ θ = ↑(-Real.pi / 2)
              source
              theorem EuclidGeom.AngValue.nsmul_toReal_eq_mul {n : ℕ} (h : n ≠ 0) {θ : EuclidGeom.AngValue} :
              EuclidGeom.AngValue.toReal (n • θ) = ↑n * EuclidGeom.AngValue.toReal θ ↔ EuclidGeom.AngValue.toReal θ ∈ Set.Ioc (-Real.pi / ↑n) (Real.pi / ↑n)
              source
              theorem EuclidGeom.AngValue.two_nsmul_toReal_eq_two_mul {θ : EuclidGeom.AngValue} :
              EuclidGeom.AngValue.toReal (2 • θ) = 2 * EuclidGeom.AngValue.toReal θ ↔ EuclidGeom.AngValue.toReal θ ∈ Set.Ioc (-Real.pi / 2) (Real.pi / 2)
              source
              theorem EuclidGeom.AngValue.two_zsmul_toReal_eq_two_mul {θ : EuclidGeom.AngValue} :
              EuclidGeom.AngValue.toReal (2 • θ) = 2 * EuclidGeom.AngValue.toReal θ ↔ EuclidGeom.AngValue.toReal θ ∈ Set.Ioc (-Real.pi / 2) (Real.pi / 2)
              source
              theorem EuclidGeom.AngValue.toReal_coe_eq_self_sub_two_mul_int_mul_pi_iff {θ : ℝ} {k : ℤ} :
              EuclidGeom.AngValue.toReal ↑θ = θ - 2 * ↑k * Real.pi ↔ θ ∈ Set.Ioc ((2 * ↑k - 1) * Real.pi) ((2 * ↑k + 1) * Real.pi)
              source
              theorem EuclidGeom.AngValue.toReal_coe_eq_self_sub_two_pi_iff {θ : ℝ} :
              EuclidGeom.AngValue.toReal ↑θ = θ - 2 * Real.pi ↔ θ ∈ Set.Ioc Real.pi (3 * Real.pi)
              source
              theorem EuclidGeom.AngValue.toReal_coe_eq_self_add_two_pi_iff {θ : ℝ} :
              EuclidGeom.AngValue.toReal ↑θ = θ + 2 * Real.pi ↔ θ ∈ Set.Ioc (-3 * Real.pi) (-Real.pi)
              source
              theorem EuclidGeom.AngValue.two_nsmul_toReal_eq_two_mul_sub_two_pi {θ : EuclidGeom.AngValue} :
              EuclidGeom.AngValue.toReal (2 • θ) = 2 * EuclidGeom.AngValue.toReal θ - 2 * Real.pi ↔ Real.pi / 2 < EuclidGeom.AngValue.toReal θ
              source
              theorem EuclidGeom.AngValue.two_zsmul_toReal_eq_two_mul_sub_two_pi {θ : EuclidGeom.AngValue} :
              EuclidGeom.AngValue.toReal (2 • θ) = 2 * EuclidGeom.AngValue.toReal θ - 2 * Real.pi ↔ Real.pi / 2 < EuclidGeom.AngValue.toReal θ
              source
              theorem EuclidGeom.AngValue.two_nsmul_toReal_eq_two_mul_add_two_pi {θ : EuclidGeom.AngValue} :
              EuclidGeom.AngValue.toReal (2 • θ) = 2 * EuclidGeom.AngValue.toReal θ + 2 * Real.pi ↔ EuclidGeom.AngValue.toReal θ ≤ -Real.pi / 2
              source
              theorem EuclidGeom.AngValue.two_zsmul_toReal_eq_two_mul_add_two_pi {θ : EuclidGeom.AngValue} :
              EuclidGeom.AngValue.toReal (2 • θ) = 2 * EuclidGeom.AngValue.toReal θ + 2 * Real.pi ↔ EuclidGeom.AngValue.toReal θ ≤ -Real.pi / 2
              source
              @[simp]
              theorem EuclidGeom.AngValue.sin_toReal (θ : EuclidGeom.AngValue) :
              Real.sin (EuclidGeom.AngValue.toReal θ) = EuclidGeom.AngValue.sin θ
              source
              @[simp]
              theorem EuclidGeom.AngValue.cos_toReal (θ : EuclidGeom.AngValue) :
              Real.cos (EuclidGeom.AngValue.toReal θ) = EuclidGeom.AngValue.cos θ
              source
              theorem EuclidGeom.AngValue.cos_nonneg_iff_abs_toReal_le_pi_div_two {θ : EuclidGeom.AngValue} :
              0 ≤ EuclidGeom.AngValue.cos θ ↔ |EuclidGeom.AngValue.toReal θ| ≤ Real.pi / 2
              source
              theorem EuclidGeom.AngValue.cos_pos_iff_abs_toReal_lt_pi_div_two {θ : EuclidGeom.AngValue} :
              0 < EuclidGeom.AngValue.cos θ ↔ |EuclidGeom.AngValue.toReal θ| < Real.pi / 2
              source
              theorem EuclidGeom.AngValue.cos_neg_iff_pi_div_two_lt_abs_toReal {θ : EuclidGeom.AngValue} :
              EuclidGeom.AngValue.cos θ < 0 ↔ Real.pi / 2 < |EuclidGeom.AngValue.toReal θ|
              source
              theorem EuclidGeom.AngValue.abs_cos_eq_abs_sin_of_two_nsmul_add_two_nsmul_eq_pi {θ : EuclidGeom.AngValue} {ψ : EuclidGeom.AngValue} (h : 2 • θ + 2 • ψ = ↑Real.pi) :
              |EuclidGeom.AngValue.cos θ| = |EuclidGeom.AngValue.sin ψ|
              source
              theorem EuclidGeom.AngValue.abs_cos_eq_abs_sin_of_two_zsmul_add_two_zsmul_eq_pi {θ : EuclidGeom.AngValue} {ψ : EuclidGeom.AngValue} (h : 2 • θ + 2 • ψ = ↑Real.pi) :
              |EuclidGeom.AngValue.cos θ| = |EuclidGeom.AngValue.sin ψ|
              source
              def EuclidGeom.AngValue.tan (θ : EuclidGeom.AngValue) :
              ℝ

              The tangent of a AngValue.

              Equations
              Instances For
                source
                theorem EuclidGeom.AngValue.tan_eq_sin_div_cos (θ : EuclidGeom.AngValue) :
                EuclidGeom.AngValue.tan θ = EuclidGeom.AngValue.sin θ / EuclidGeom.AngValue.cos θ
                source
                @[simp]
                theorem EuclidGeom.AngValue.tan_coe (x : ℝ) :
                EuclidGeom.AngValue.tan ↑x = Real.tan x
                source
                @[simp]
                theorem EuclidGeom.AngValue.tan_zero :
                EuclidGeom.AngValue.tan 0 = 0
                source
                theorem EuclidGeom.AngValue.tan_coe_pi :
                EuclidGeom.AngValue.tan ↑Real.pi = 0
                source
                theorem EuclidGeom.AngValue.tan_periodic :
                Function.Periodic EuclidGeom.AngValue.tan ↑Real.pi
                source
                @[simp]
                theorem EuclidGeom.AngValue.tan_add_pi (θ : EuclidGeom.AngValue) :
                EuclidGeom.AngValue.tan (θ + ↑Real.pi) = EuclidGeom.AngValue.tan θ
                source
                @[simp]
                theorem EuclidGeom.AngValue.tan_sub_pi (θ : EuclidGeom.AngValue) :
                EuclidGeom.AngValue.tan (θ - ↑Real.pi) = EuclidGeom.AngValue.tan θ
                source
                @[simp]
                theorem EuclidGeom.AngValue.tan_toReal (θ : EuclidGeom.AngValue) :
                Real.tan (EuclidGeom.AngValue.toReal θ) = EuclidGeom.AngValue.tan θ
                source
                theorem EuclidGeom.AngValue.tan_eq_of_two_nsmul_eq {θ : EuclidGeom.AngValue} {ψ : EuclidGeom.AngValue} (h : 2 • θ = 2 • ψ) :
                EuclidGeom.AngValue.tan θ = EuclidGeom.AngValue.tan ψ
                source
                theorem EuclidGeom.AngValue.tan_eq_of_two_zsmul_eq {θ : EuclidGeom.AngValue} {ψ : EuclidGeom.AngValue} (h : 2 • θ = 2 • ψ) :
                EuclidGeom.AngValue.tan θ = EuclidGeom.AngValue.tan ψ
                source
                theorem EuclidGeom.AngValue.tan_eq_inv_of_two_nsmul_add_two_nsmul_eq_pi {θ : EuclidGeom.AngValue} {ψ : EuclidGeom.AngValue} (h : 2 • θ + 2 • ψ = ↑Real.pi) :
                EuclidGeom.AngValue.tan ψ = (EuclidGeom.AngValue.tan θ)⁻¹
                source
                theorem EuclidGeom.AngValue.tan_eq_inv_of_two_zsmul_add_two_zsmul_eq_pi {θ : EuclidGeom.AngValue} {ψ : EuclidGeom.AngValue} (h : 2 • θ + 2 • ψ = ↑Real.pi) :
                EuclidGeom.AngValue.tan ψ = (EuclidGeom.AngValue.tan θ)⁻¹
                source
                def EuclidGeom.AngValue.sign (θ : EuclidGeom.AngValue) :
                SignType

                The sign of a AngValue is 0 if the angle is 0 or π, 1 if the angle is strictly between 0 and π and -1 is the angle is strictly between -π and 0. It is defined as the sign of the sine of the angle.

                Equations
                Instances For
                  source
                  @[simp]
                  theorem EuclidGeom.AngValue.sign_zero :
                  EuclidGeom.AngValue.sign 0 = 0
                  source
                  @[simp]
                  theorem EuclidGeom.AngValue.sign_coe_pi :
                  EuclidGeom.AngValue.sign ↑Real.pi = 0
                  source
                  @[simp]
                  theorem EuclidGeom.AngValue.sign_neg (θ : EuclidGeom.AngValue) :
                  EuclidGeom.AngValue.sign (-θ) = -EuclidGeom.AngValue.sign θ
                  source
                  theorem EuclidGeom.AngValue.sign_antiperiodic :
                  Function.Antiperiodic EuclidGeom.AngValue.sign ↑Real.pi
                  source
                  @[simp]
                  theorem EuclidGeom.AngValue.sign_add_pi (θ : EuclidGeom.AngValue) :
                  EuclidGeom.AngValue.sign (θ + ↑Real.pi) = -EuclidGeom.AngValue.sign θ
                  source
                  @[simp]
                  theorem EuclidGeom.AngValue.sign_pi_add (θ : EuclidGeom.AngValue) :
                  EuclidGeom.AngValue.sign (↑Real.pi + θ) = -EuclidGeom.AngValue.sign θ
                  source
                  @[simp]
                  theorem EuclidGeom.AngValue.sign_sub_pi (θ : EuclidGeom.AngValue) :
                  EuclidGeom.AngValue.sign (θ - ↑Real.pi) = -EuclidGeom.AngValue.sign θ
                  source
                  @[simp]
                  theorem EuclidGeom.AngValue.sign_pi_sub (θ : EuclidGeom.AngValue) :
                  EuclidGeom.AngValue.sign (↑Real.pi - θ) = EuclidGeom.AngValue.sign θ
                  source
                  theorem EuclidGeom.AngValue.sign_eq_zero_iff {θ : EuclidGeom.AngValue} :
                  EuclidGeom.AngValue.sign θ = 0 ↔ θ = 0 ∨ θ = ↑Real.pi
                  source
                  theorem EuclidGeom.AngValue.sign_ne_zero_iff {θ : EuclidGeom.AngValue} :
                  EuclidGeom.AngValue.sign θ ≠ 0 ↔ θ ≠ 0 ∧ θ ≠ ↑Real.pi
                  source
                  theorem EuclidGeom.AngValue.toReal_neg_iff_sign_neg {θ : EuclidGeom.AngValue} :
                  EuclidGeom.AngValue.toReal θ < 0 ↔ EuclidGeom.AngValue.sign θ = -1
                  source
                  theorem EuclidGeom.AngValue.toReal_nonneg_iff_sign_nonneg {θ : EuclidGeom.AngValue} :
                  0 ≤ EuclidGeom.AngValue.toReal θ ↔ 0 ≤ EuclidGeom.AngValue.sign θ
                  source
                  @[simp]
                  theorem EuclidGeom.AngValue.sign_toReal {θ : EuclidGeom.AngValue} (h : θ ≠ ↑Real.pi) :
                  SignType.sign (EuclidGeom.AngValue.toReal θ) = EuclidGeom.AngValue.sign θ
                  source
                  theorem EuclidGeom.AngValue.coe_abs_toReal_of_sign_nonneg {θ : EuclidGeom.AngValue} (h : 0 ≤ EuclidGeom.AngValue.sign θ) :
                  ↑|EuclidGeom.AngValue.toReal θ| = θ
                  source
                  theorem EuclidGeom.AngValue.neg_coe_abs_toReal_of_sign_nonpos {θ : EuclidGeom.AngValue} (h : EuclidGeom.AngValue.sign θ ≤ 0) :
                  -↑|EuclidGeom.AngValue.toReal θ| = θ
                  source
                  theorem EuclidGeom.AngValue.eq_iff_sign_eq_and_abs_toReal_eq {θ : EuclidGeom.AngValue} {ψ : EuclidGeom.AngValue} :
                  θ = ψ ↔ EuclidGeom.AngValue.sign θ = EuclidGeom.AngValue.sign ψ ∧ |EuclidGeom.AngValue.toReal θ| = |EuclidGeom.AngValue.toReal ψ|
                  source
                  theorem EuclidGeom.AngValue.eq_iff_abs_toReal_eq_of_sign_eq {θ : EuclidGeom.AngValue} {ψ : EuclidGeom.AngValue} (h : EuclidGeom.AngValue.sign θ = EuclidGeom.AngValue.sign ψ) :
                  θ = ψ ↔ |EuclidGeom.AngValue.toReal θ| = |EuclidGeom.AngValue.toReal ψ|
                  source
                  @[simp]
                  theorem EuclidGeom.AngValue.sign_coe_pi_div_two :
                  EuclidGeom.AngValue.sign ↑(Real.pi / 2) = 1
                  source
                  @[simp]
                  theorem EuclidGeom.AngValue.sign_coe_neg_pi_div_two :
                  EuclidGeom.AngValue.sign ↑(-Real.pi / 2) = -1
                  source
                  theorem EuclidGeom.AngValue.sign_coe_nonneg_of_nonneg_of_le_pi {θ : ℝ} (h0 : 0 ≤ θ) (hpi : θ ≤ Real.pi) :
                  0 ≤ EuclidGeom.AngValue.sign ↑θ
                  source
                  theorem EuclidGeom.AngValue.sign_neg_coe_nonpos_of_nonneg_of_le_pi {θ : ℝ} (h0 : 0 ≤ θ) (hpi : θ ≤ Real.pi) :
                  EuclidGeom.AngValue.sign (-↑θ) ≤ 0
                  source
                  theorem EuclidGeom.AngValue.sign_two_nsmul_eq_sign_iff {θ : EuclidGeom.AngValue} :
                  EuclidGeom.AngValue.sign (2 • θ) = EuclidGeom.AngValue.sign θ ↔ θ = ↑Real.pi ∨ |EuclidGeom.AngValue.toReal θ| < Real.pi / 2
                  source
                  theorem EuclidGeom.AngValue.sign_two_zsmul_eq_sign_iff {θ : EuclidGeom.AngValue} :
                  EuclidGeom.AngValue.sign (2 • θ) = EuclidGeom.AngValue.sign θ ↔ θ = ↑Real.pi ∨ |EuclidGeom.AngValue.toReal θ| < Real.pi / 2
                  source
                  theorem EuclidGeom.AngValue.continuousAt_sign {θ : EuclidGeom.AngValue} (h0 : θ ≠ 0) (hpi : θ ≠ ↑Real.pi) :
                  ContinuousAt EuclidGeom.AngValue.sign θ
                  source
                  theorem ContinuousOn.angValue_sign_comp {α : Type u_1} [TopologicalSpace α] {f : α → EuclidGeom.AngValue} {s : Set α} (hf : ContinuousOn f s) (hs : ∀ z ∈ s, f z ≠ 0 ∧ f z ≠ ↑Real.pi) :
                  ContinuousOn (EuclidGeom.AngValue.sign ∘ f) s
                  source
                  theorem EuclidGeom.AngValue.sign_eq_of_continuousOn {α : Type u_1} [TopologicalSpace α] {f : α → EuclidGeom.AngValue} {s : Set α} {x : α} {y : α} (hc : IsConnected s) (hf : ContinuousOn f s) (hs : ∀ z ∈ s, f z ≠ 0 ∧ f z ≠ ↑Real.pi) (hx : x ∈ s) (hy : y ∈ s) :
                  EuclidGeom.AngValue.sign (f y) = EuclidGeom.AngValue.sign (f x)

                  Suppose a function to angles is continuous on a connected set and never takes the values 0 or π on that set. Then the values of the function on that set all have the same sign.

                  source
                  @[simp]
                  theorem Complex.arg_conj_coe_angValue (x : ℂ) :
                  ↑(Complex.arg ((starRingEnd ℂ) x)) = -↑(Complex.arg x)
                  source
                  @[simp]
                  theorem Complex.arg_inv_coe_angValue (x : ℂ) :
                  ↑(Complex.arg x⁻¹) = -↑(Complex.arg x)
                  source
                  theorem Complex.arg_neg_coe_angValue {x : ℂ} (hx : x ≠ 0) :
                  ↑(Complex.arg (-x)) = ↑(Complex.arg x) + ↑Real.pi
                  source
                  theorem Complex.arg_mul_cos_add_sin_mul_I_coe_angValue {r : ℝ} (hr : 0 < r) (θ : EuclidGeom.AngValue) :
                  ↑(Complex.arg (↑r * (↑(EuclidGeom.AngValue.cos θ) + ↑(EuclidGeom.AngValue.sin θ) * Complex.I))) = θ
                  source
                  @[simp]
                  theorem Complex.arg_cos_add_sin_mul_I_coe_angValue (θ : EuclidGeom.AngValue) :
                  ↑(Complex.arg (↑(EuclidGeom.AngValue.cos θ) + ↑(EuclidGeom.AngValue.sin θ) * Complex.I)) = θ
                  source
                  theorem Complex.arg_mul_coe_angValue {x : ℂ} {y : ℂ} (hx : x ≠ 0) (hy : y ≠ 0) :
                  ↑(Complex.arg (x * y)) = ↑(Complex.arg x) + ↑(Complex.arg y)
                  source
                  theorem Complex.arg_div_coe_angValue {x : ℂ} {y : ℂ} (hx : x ≠ 0) (hy : y ≠ 0) :
                  ↑(Complex.arg (x / y)) = ↑(Complex.arg x) - ↑(Complex.arg y)
                  source
                  @[simp]
                  theorem Complex.arg_coe_angValue_toReal_eq_arg (z : ℂ) :
                  EuclidGeom.AngValue.toReal ↑(Complex.arg z) = Complex.arg z
                  source
                  theorem Complex.arg_coe_angValue_eq_iff_eq_toReal {z : ℂ} {θ : EuclidGeom.AngValue} :
                  ↑(Complex.arg z) = θ ↔ Complex.arg z = EuclidGeom.AngValue.toReal θ
                  source
                  @[simp]
                  theorem Complex.arg_coe_angValue_eq_iff {x : ℂ} {y : ℂ} :
                  ↑(Complex.arg x) = ↑(Complex.arg y) ↔ Complex.arg x = Complex.arg y
                  source
                  theorem Complex.continuousAt_arg_coe_angValue {x : ℂ} (h : x ≠ 0) :
                  ContinuousAt (EuclidGeom.AngValue.coe ∘ Complex.arg) x
                  source
                  noncomputable def EuclidGeom.AngValue.expMapCircle (θ : EuclidGeom.AngValue) :
                  ↥circle

                  expMapCircle, applied to a AngValue.

                  Equations
                  Instances For
                    source
                    @[simp]
                    theorem EuclidGeom.AngValue.expMapCircle_coe (x : ℝ) :
                    EuclidGeom.AngValue.expMapCircle ↑x = expMapCircle x
                    source
                    theorem EuclidGeom.AngValue.coe_expMapCircle (θ : EuclidGeom.AngValue) :
                    ↑(EuclidGeom.AngValue.expMapCircle θ) = ↑(EuclidGeom.AngValue.cos θ) + ↑(EuclidGeom.AngValue.sin θ) * Complex.I
                    source
                    @[simp]
                    theorem EuclidGeom.AngValue.expMapCircle_zero :
                    EuclidGeom.AngValue.expMapCircle 0 = 1
                    source
                    @[simp]
                    theorem EuclidGeom.AngValue.expMapCircle_neg (θ : EuclidGeom.AngValue) :
                    EuclidGeom.AngValue.expMapCircle (-θ) = (EuclidGeom.AngValue.expMapCircle θ)⁻¹
                    source
                    @[simp]
                    theorem EuclidGeom.AngValue.expMapCircle_add (θ₁ : EuclidGeom.AngValue) (θ₂ : EuclidGeom.AngValue) :
                    EuclidGeom.AngValue.expMapCircle (θ₁ + θ₂) = EuclidGeom.AngValue.expMapCircle θ₁ * EuclidGeom.AngValue.expMapCircle θ₂
                    source
                    @[simp]
                    theorem EuclidGeom.AngValue.arg_expMapCircle (θ : EuclidGeom.AngValue) :
                    ↑(Complex.arg ↑(EuclidGeom.AngValue.expMapCircle θ)) = θ