`reciprocal`

definition

show as: view math explainer →

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

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

 795      rfl⟩
 796
 797/-- The reciprocal automorphism. -/
 798noncomputable def reciprocal : JAut :=
 799  ⟨posInv, by
 800    constructor
 801    · intro x y
 802      apply Subtype.ext
 803      simp [posMul, posInv, mul_comm]
 804    · intro x
 805      simpa [posInv] using (J_reciprocal x.1 x.2).symm⟩
 806
 807/-- Composition of `J`-automorphisms. -/
 808def comp (g f : JAut) : JAut :=
 809  ⟨fun x => g (f x), by
 810    constructor
 811    · intro x y
 812      change g (f (posMul x y)) = posMul (g (f x)) (g (f y))
 813      rw [f.multiplicative x y, g.multiplicative (f x) (f y)]
 814    · intro x
 815      rw [g.preserves_cost (f x), f.preserves_cost x]⟩
 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

papers checked against this theorem

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