theorem proved term proof

`samePattern_symm`

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

formal statement (Lean)

  93theorem samePattern_symm {O₁ O₂ : Octave} (h : samePattern O₁ O₂) :
  94    samePattern O₂ O₁ :=

Term-mode proof.

  95  let ⟨e⟩ := h
  96  ⟨OctaveEquiv.symm e⟩
  97
  98end RRF.Theorems
  99end IndisputableMonolith

Lean names referenced from this declaration's body.