Namespace `GL2F3` 1 theorems

Order-8 elements of GL₂(mathbb F₃) are conjugate to their cubes GL2F3.isConj_pow_three_of_orderOf_eq_eight 0 below · cited by 1 · depth 16

Documents the Lean sources in this repository (Lean v4.33.1, Mathlib v4.33.0). Statements are quoted textually from the .lean files; dependency edges are the import Theorems.Thm_… lines of the proof modules. About these pages.

Namespace GL2F3 1 theorems

Namespace `GL2F3` 1 theorems