`posInv_two`

proved

show as: view math explainer →

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

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

formal source

 752  apply Subtype.ext
 753  simp [posInv, posOne]
 754
 755@[simp] theorem posInv_two : posInv posTwo = posHalf := by
 756  apply Subtype.ext
 757  norm_num [posInv, posTwo, posHalf]
 758
 759@[simp] theorem posInv_half : posInv posHalf = posTwo := by
 760  apply Subtype.ext
 761  norm_num [posInv, posTwo, posHalf]
 762
 763/-- The honest automorphism type of the canonical cost algebra on `ℝ_{>0}`. -/
 764def JAut : Type :=
 765  { f : PosReal → PosReal //
 766      (∀ x y : PosReal, f (posMul x y) = posMul (f x) (f y)) ∧
 767      (∀ x : PosReal, J (f x).1 = J x.1) }
 768
 769namespace JAut
 770
 771instance : CoeFun JAut (fun _ => PosReal → PosReal) := ⟨fun f => f.1⟩
 772
 773/-- Multiplicativity of a `J`-automorphism. -/
 774theorem multiplicative (f : JAut) (x y : PosReal) :
 775    f (posMul x y) = posMul (f x) (f y) :=
 776  f.2.1 x y
 777
 778/-- Cost preservation of a `J`-automorphism. -/
 779theorem preserves_cost (f : JAut) (x : PosReal) :
 780    J (f x).1 = J x.1 :=
 781  f.2.2 x
 782
 783@[ext] theorem ext {f g : JAut} (h : ∀ x : PosReal, f x = g x) : f = g := by
 784  apply Subtype.ext
 785  funext x

papers checked against this theorem

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