`comp_id`

proved

show as: view math explainer →

module: IndisputableMonolith.Algebra.CostAlgebra
domain: Algebra
line: 819 · 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 819.

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

 816
 817@[simp] theorem comp_apply (g f : JAut) (x : PosReal) : comp g f x = g (f x) := rfl
 818
 819@[simp] theorem comp_id (f : JAut) : comp id f = f := by
 820  apply JAut.ext
 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

papers checked against this theorem

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