pith. machine review for the scientific record. sign in
def definition def or abbrev

reciprocal

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 798noncomputable def reciprocal : JAut :=

proof body

Definition body.

 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. -/

used by (40)

From the project-wide theorem graph. These declarations reference this one in their body.

… and 10 more

depends on (12)

Lean names referenced from this declaration's body.