Frobenius theorem (real division algebras)

Stream: mathlib4

[Weiyi Wang]

As I continue practicing Lean with some fun theorems, I formalized a proof for Frobenius theorem (finite dimensional division algebra over real can only be real, complex, or quaternion) at https://github.com/wwylele/mathlib4/blob/algebra-frobenius/Mathlib/Algebra/Algebra/Real.lean, though because I cared little about code quality, right now it looks like a shitpost :face_with_peeking_eye: I'll need to clean up a lot of things

So a few questions:

• This is not yet in mathlib and we want it, right?
• I followed some textbook proof similar to the one in wikipedia, with a few shortcuts taken. Is this optimal, or there is some higher level theory in mathlib that could create a much shorter proof?
• other questions that I can find answers myself, but suggests are also welcome: theorem names? locations?

[Aaron Liu]

set_option maxHeartbeats 800000
What's so expensive?

[Weiyi Wang]

Probably just being long and the fin_cases at the end...

[Aaron Liu]

Wow, does that one theorem take up 500 lines? That's like half the mathlib long file limit

[Weiyi Wang]

lol, as I said, the code quality is pretty low at the moment. It definitely can be split up

[Weiyi Wang]

I guess I shouls make use of QuaternionAlgebra.Basis, though it doesn't have AlgEquiv yet

[Eric Wieser]

I think @Edison Xie has a proof of this too

[Weiyi Wang]

I'd love to see how he did it

While trying to split the proof into smaller ones, I found it cumbersome because a lot of intermediate result depends on a hypothesis ("the dimension of D is at least 3" or equivalent). Attaching the hypothesis to def and lemma is pretty verbose. Is this where I should add a [Fact h] locally just to reduce the verbosity?

[Michael Rothgang]

Do you know about the variable command? (Looking at your message, I'm not sure if you do.)

[Michael Rothgang]

If you do: can you give an example what you're talking about? That would make it easier to help you.

[Weiyi Wang]

I know half of it. I guess you are hinting that I can make a variable {h :...} so it get carried around implicitly. I'll give a try

[Weiyi Wang]

hmm, the problem with variable {h :...} (or having {h : ...} in general) is that it doesn't automatically get passed around across lemmas. For example

variable {h : ∃ n, n = 21}

noncomputable
def i : Nat := h.choose

theorem i_prop : i * 2 = 42 := by sorry -- don't know how to synthesize implicit argument 'h'
theorem i_prop2 {h : ∃ n, n = 21} : i * 2 = 42 := by sorry -- don't know how to synthesize implicit argument 'h'
theorem i_prop3 : i (h := h) * 2  = 42 := by sorry -- ok

That's why I thought about using instance resolution with Fact to pass it around instead.
It's not a big deal. In the end I could just explicitly specify everything. Just want to look for better code style

[Edison Xie]

Weiyi Wang said:

I'd love to see how he did it

By introducing subfield and relying on some facts about it, I will PR it as soon as I figure out whether we need to generalise IntermediateField to non-commutative case or we add some CommSubalgebra and DivisionSubalgebra

[Edison Xie]

also we need some results about quaternion bases, but if you're interested you are very welcome to checkout my (not-so-secret) Brauer group repo