 910    simpa [comp, reciprocal, id] using hx'
 911
 912/-- A two-point coding of `Aut(J)`. -/
 913noncomputable def equivFinTwo : JAut ≃ Fin 2 := by
 914  classical
 915  refine
 916    { toFun := fun f => if f = id then 0 else 1
 917      invFun := fun i => if i = 0 then id else reciprocal
 918      left_inv := ?_
 919      right_inv := ?_ }
 920  · intro f
 921    rcases eq_id_or_reciprocal f with h | h
 922    · simp [h]
 923    · simp [h, reciprocal_ne_id]
 924  · intro i
 925    fin_cases i <;> simp [reciprocal_ne_id]
 926
 927/-- **Closed automorphism theorem**: `Aut(J)` is exactly `ℤ/2ℤ`. -/
 928noncomputable def equivZModTwo : JAut ≃ ZMod 2 :=
 929  equivFinTwo.trans (ZMod.finEquiv 2).toEquiv
 930
 931end JAut
 932
 933/-- Paper-facing closed automorphism theorem:
 934    the only continuous multiplicative bijections on `ℝ_{>0}` preserving `J`
 935    are the identity and reciprocal maps. The continuity and bijectivity
 936    assumptions are stronger than needed; the proof uses the sharper `JAut`
 937    classification above. -/
 938theorem continuous_bijective_preserves_J_eq_id_or_inv
 939    {f : PosReal → PosReal} (_hCont : Continuous f) (_hBij : Function.Bijective f)
 940    (hmul : ∀ x y : PosReal, f (posMul x y) = posMul (f x) (f y))
 941    (hJ : ∀ x : PosReal, J (f x).1 = J x.1) :
 942    f = (fun x => x) ∨ f = posInv := by
 943  let g : JAut := ⟨f, ⟨hmul, hJ⟩⟩

papers checked against this theorem

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