`posInv_two`

proved

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Algebra.CostAlgebra on GitHub at line 755.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

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.