OAI/RingTheory/DirectFiniteness/Main.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KaplanskyCounterexample.main_theorem line 9

   Source documentation

   A finite field of characteristic two and a finitely generated group admit finite group-algebra sums with a right inverse that is not a left inverse.

   Distinct definitions of this name: ComparatorChallenges/KaplanskyDirectFiniteness.lean:12 (same statement text; different proof or body). Qualify references as OAI.KaplanskyCounterexample.main_theorem@path.

   theorem main_theorem : MainClaim := Prescription.Output.prescribed_main
   …

   Mentions: OAI.KaplanskyCounterexample.MainClaim, OAI.KaplanskyCounterexample.Prescription.Output.prescribed_main