`JAut`

definition

show as: view math explainer →

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

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

 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
 786  exact h x
 787
 788/-- The identity automorphism. -/
 789def id : JAut :=
 790  ⟨fun x => x, by
 791    constructor
 792    · intro _ _
 793      rfl
 794    · intro _

papers checked against this theorem

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