theorem endomorphism_bijective_of_ne_zero {A : Type u} [Ring A] {M : Type u} [AddCommGroup M] [Module A M] [IsSimpleModule A M] (f : Module.End A M) (hf : f ≠ 0) : Function.Bijective ⇑f

@[implicit_reducible]

noncomputable instance endDivisionRing {A : Type u} [Ring A] {M : Type u} [AddCommGroup M] [Module A M] [IsSimpleModule A M] : DivisionRing (Module.End A M)

theorem algebraic_in_range_of_algClosed (k : Type u) [Field k] [IsAlgClosed k] (D : Type u) [DivisionRing D] [Algebra k D] (x : D) (hx : IsAlgebraic k x) : x ∈ Set.range ⇑(algebraMap k D)

theorem x_sub_ne_zero_of_transcendental {k : Type u} [Field k] {D : Type u} [DivisionRing D] [Algebra k D] {x : D} (hx : Transcendental k x) (a : k) : x - (algebraMap k D) a ≠ 0

theorem linearIndependent_resolvent (k : Type u) [Field k] (D : Type u) [DivisionRing D] [Algebra k D] (x : D) (hx : Transcendental k x) : LinearIndependent k fun (a : k) => (x - (algebraMap k D) a)⁻¹

def evalAt {k : Type u} [CommSemiring k] (A : Type u) [Semiring A] [Algebra k A] {M : Type u} [AddCommMonoid M] [Module A M] [Module k M] [IsScalarTower k A M] (v : M) : Module.End A M →ₗ[k] M

theorem evalAt_injective {k : Type u} [Field k] (A : Type u) [Ring A] [Algebra k A] {M : Type u} [AddCommGroup M] [Module A M] [Module k M] [IsScalarTower k A M] [IsSimpleModule A M] (v : M) (hv : v ≠ 0) : Function.Injective ⇑(evalAt A v)

def smulMap {k : Type u} [CommSemiring k] (A : Type u) [Semiring A] [Algebra k A] {M : Type u} [AddCommMonoid M] [Module A M] [Module k M] [IsScalarTower k A M] (v : M) : A →ₗ[k] M

theorem smulMap_surjective {k : Type u} [Field k] (A : Type u) [Ring A] [Algebra k A] {M : Type u} [AddCommGroup M] [Module A M] [Module k M] [IsScalarTower k A M] [IsSimpleModule A M] (v : M) (hv : v ≠ 0) : Function.Surjective ⇑(smulMap A v)

theorem dixmier_lemma (k : Type u) [Field k] [IsAlgClosed k] (A : Type u) [Ring A] [Algebra k A] (M : Type u) [AddCommGroup M] [Module A M] [Module k M] [IsScalarTower k A M] [IsSimpleModule A M] (hA : Module.rank k A ≤ Cardinal.aleph0) (hunc : Cardinal.aleph0 < Cardinal.mk k) : Function.Bijective ⇑(algebraMap k (Module.End A M))

def centerToEnd {k : Type u} [Field k] (A : Type u) [Ring A] [Algebra k A] {M : Type u} [AddCommGroup M] [Module A M] [Module k M] [IsScalarTower k A M] : ↥(Subalgebra.center k A) →ₐ[k] Module.End A M

noncomputable def centerCharacter {k : Type u} [Field k] (A : Type u) [Ring A] [Algebra k A] {M : Type u} [AddCommGroup M] [Module A M] [Module k M] [IsScalarTower k A M] (hbij : Function.Bijective ⇑(algebraMap k (Module.End A M))) : ↥(Subalgebra.center k A) →ₐ[k] k

theorem center_acts_by_character {k : Type u} [Field k] (A : Type u) [Ring A] [Algebra k A] {M : Type u} [AddCommGroup M] [Module A M] [Module k M] [IsScalarTower k A M] (hbij : Function.Bijective ⇑(algebraMap k (Module.End A M))) (z : ↥(Subalgebra.center k A)) (m : M) : ↑z • m = (centerCharacter A hbij) z • m

theorem dixmier_lemma_center_character (k : Type u) [Field k] [IsAlgClosed k] (A : Type u) [Ring A] [Algebra k A] (M : Type u) [AddCommGroup M] [Module A M] [Module k M] [IsScalarTower k A M] [IsSimpleModule A M] (hA : Module.rank k A ≤ Cardinal.aleph0) (hunc : Cardinal.aleph0 < Cardinal.mk k) : ∃ (χ : ↥(Subalgebra.center k A) →ₐ[k] k), ∀ (z : ↥(Subalgebra.center k A)) (m : M), ↑z • m = χ z • m