English
Over an algebraically closed field F, a finite-dimensional simple algebra is isomorphic to a matrix algebra M_n(F).
Русский
Над алгеброй F, полным замыканием, простая конечнодименсиональная алгебра изоморфна M_n(F).
LaTeX
$$[IsSimpleRing R] [FiniteDimensional F R] ⇒ ∃ n (hn: NeZero n), Nonempty (R ≃ₐ[F] Matrix(Fin n)(Fin n) F).$$
Lean4
/-- The **Wedderburn–Artin Theorem** over algebraically closed fields: a finite-dimensional
semisimple algebra over an algebraically closed field is isomorphic to a product of matrix algebras
over the field. -/
theorem exists_algEquiv_pi_matrix_of_isAlgClosed [IsSemisimpleRing R] [FiniteDimensional F R] :
∃ (n : ℕ) (d : Fin n → ℕ), (∀ i, NeZero (d i)) ∧ Nonempty (R ≃ₐ[F] Π i, Matrix (Fin (d i)) (Fin (d i)) F) :=
have ⟨n, D, d, _, _, _, hd, ⟨e⟩⟩ := exists_algEquiv_pi_matrix_divisionRing_finite F R
⟨n, d, hd,
⟨e.trans <|
.piCongrRight fun i ↦
.mapMatrix <| .symm <| .ofBijective (Algebra.ofId F (D i)) IsAlgClosed.algebraMap_bijective_of_isIntegral⟩⟩
