913noncomputable def equivFinTwo : JAut ≃ Fin 2 := by
proof body
Definition body.
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ℤ`. -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.