`id_comp`

proved

show as: view math explainer →

module: IndisputableMonolith.Algebra.CostAlgebra
domain: Algebra
line: 824 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Algebra.CostAlgebra on GitHub at line 824.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

 821  intro x
 822  rfl
 823
 824@[simp] theorem id_comp (f : JAut) : comp f id = f := by
 825  apply JAut.ext
 826  intro x
 827  rfl
 828
 829@[simp] theorem reciprocal_comp_reciprocal : comp reciprocal reciprocal = id := by
 830  apply JAut.ext
 831  intro x
 832  simp [comp, reciprocal, id]
 833
 834/-- Pointwise, a `J`-automorphism can only choose the identity branch or the
 835    reciprocal branch. -/
 836theorem eq_self_or_inv (f : JAut) (x : PosReal) :
 837    f x = x ∨ f x = posInv x := by
 838  have hJ : J (f x).1 = J x.1 := f.preserves_cost x
 839  rcases (J_eq_iff_eq_or_inv x.2 (f x).2).mp hJ with h | h
 840  · left
 841    exact Subtype.ext h
 842  · right
 843    exact Subtype.ext h
 844
 845/-- If `2 * x⁻¹ = 2 * x`, positivity forces `x = 1`. -/
 846theorem two_mul_inv_eq_two_mul_iff (x : PosReal) :
 847    posMul posTwo (posInv x) = posMul posTwo x ↔ x = posOne := by
 848  constructor
 849  · intro h
 850    apply Subtype.ext
 851    have hval : (2 : ℝ) * (x : ℝ)⁻¹ = 2 * (x : ℝ) := congrArg Subtype.val h
 852    have hx0 : (x : ℝ) ≠ 0 := ne_of_gt x.2
 853    field_simp [hx0] at hval
 854    have hsq : (x : ℝ) ^ 2 = 1 := by linarith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.