theorem IsFractionRing.stabilizerHom_surjective.{u_1,
    u_2, u_3, u_4, u_5}
  {AType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } {BType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  [CommRingCommRing.{u} (α : Type u) : Type uA commutative ring is a ring with commutative multiplication.  AType u_1] [CommRingCommRing.{u} (α : Type u) : Type uA commutative ring is a ring with commutative multiplication.  BType u_2] [AlgebraAlgebra.{u, v} (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] : Type (max u v)An associative unital `R`-algebra is a semiring `A` equipped with a map into its center `R → A`.

See the implementation notes in this file for discussion of the details of this definition.
 AType u_1 BType u_2]
  (GType u_3 : Type u_3A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) [GroupGroup.{u} (G : Type u) : Type uA `Group` is a `Monoid` with an operation `⁻¹` satisfying `a⁻¹ * a = 1`.

There is also a division operation `/` such that `a / b = a * b⁻¹`,
with a default so that `a / b = a * b⁻¹` holds by definition.

Use `Group.ofLeftAxioms` or `Group.ofRightAxioms` to define a group structure
on a type with the minimum proof obligations.
 GType u_3] [FiniteFinite.{u_3} (α : Sort u_3) : PropA type is `Finite` if it is in bijective correspondence to some `Fin n`.

This is similar to `Fintype`, but `Finite` is a proposition rather than data.
A particular benefit to this is that `Finite` instances are definitionally equal to one another
(due to proof irrelevance) rather than being merely propositionally equal,
and, furthermore, `Finite` instances generally avoid the need for `Decidable` instances.
One other notable difference is that `Finite` allows there to be `Finite p` instances
for all `p : Prop`, which is not allowed by `Fintype` due to universe constraints.
An application of this is that `Finite (x ∈ s → β x)` follows from the general instance for pi
types, assuming `[∀ x, Finite (β x)]`.
Implementation note: this is a reason `Finite α` is not defined as `Nonempty (Fintype α)`.

Every `Fintype` instance provides a `Finite` instance via `Finite.of_fintype`.
Conversely, one can noncomputably create a `Fintype` instance from a `Finite` instance
via `Fintype.ofFinite`. In a proof one might write
```lean
  have := Fintype.ofFinite α
```
to obtain such an instance.

Do not write noncomputable `Fintype` instances; instead write `Finite` instances
and use this `Fintype.ofFinite` interface.
The `Fintype` instances should be relied upon to be computable for evaluation purposes.

Theorems should use `Finite` instead of `Fintype`, unless definitions in the theorem statement
require `Fintype`.
Definitions should prefer `Finite` as well, unless it is important that the definitions
are meant to be computable in the reduction or `#eval` sense.
 GType u_3]
  [MulSemiringActionMulSemiringAction.{u, v} (M : Type u) (R : Type v) [Monoid M] [Semiring R] : Type (max u v)Typeclass for multiplicative actions by monoids on semirings.

This combines `DistribMulAction` with `MulDistribMulAction`: it expresses
the interplay between the action and both addition and multiplication on the target.
Two key axioms are `g • (x + y) = (g • x) + (g • y)` and `g • (x * y) = (g • x) * (g • y)`.

A typical use case is the action of a Galois group $Gal(L/K)$ on the field `L`.
 GType u_3 BType u_2]
  [SMulCommClassSMulCommClass.{u_9, u_10, u_11} (M : Type u_9) (N : Type u_10) (α : Type u_11) [SMul M α] [SMul N α] : PropA typeclass mixin saying that two multiplicative actions on the same space commute.  GType u_3 AType u_1 BType u_2] (PIdeal A : IdealIdeal.{u} (R : Type u) [Semiring R] : Type uA (left) ideal in a semiring `R` is an additive submonoid `s` such that
`a * b ∈ s` whenever `b ∈ s`. If `R` is a ring, then `s` is an additive subgroup.  AType u_1)
  (QIdeal B : IdealIdeal.{u} (R : Type u) [Semiring R] : Type uA (left) ideal in a semiring `R` is an additive submonoid `s` such that
`a * b ∈ s` whenever `b ∈ s`. If `R` is a ring, then `s` is an additive subgroup.  BType u_2) [QIdeal B.IsPrimeIdeal.IsPrime.{u} {α : Type u} [Semiring α] (I : Ideal α) : PropAn ideal `P` of a ring `R` is prime if `P ≠ R` and `xy ∈ P → x ∈ P ∨ y ∈ P` ] [QIdeal B.LiesOverIdeal.LiesOver.{u_2, u_3} {A : Type u_2} [CommSemiring A] {B : Type u_3} [Semiring B] [Algebra A B] (P : Ideal B)
  (p : Ideal A) : Prop`P` lies over `p` if `p` is the preimage of `P` by the `algebraMap`.  PIdeal A]
  (KType u_4 : Type u_4A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) (LType u_5 : Type u_5A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) [FieldField.{u} (K : Type u) : Type uA `Field` is a `CommRing` with multiplicative inverses for nonzero elements.

An instance of `Field K` includes maps `ratCast : ℚ → K` and `qsmul : ℚ → K → K`.
Those two fields are needed to implement the `DivisionRing K → Algebra ℚ K` instance since we need
to control the specific definitions for some special cases of `K` (in particular `K = ℚ` itself).
See also note [forgetful inheritance].

If the field has positive characteristic `p`, our division by zero convention forces
`ratCast (1 / p) = 1 / 0 = 0`.  KType u_4]
  [FieldField.{u} (K : Type u) : Type uA `Field` is a `CommRing` with multiplicative inverses for nonzero elements.

An instance of `Field K` includes maps `ratCast : ℚ → K` and `qsmul : ℚ → K → K`.
Those two fields are needed to implement the `DivisionRing K → Algebra ℚ K` instance since we need
to control the specific definitions for some special cases of `K` (in particular `K = ℚ` itself).
See also note [forgetful inheritance].

If the field has positive characteristic `p`, our division by zero convention forces
`ratCast (1 / p) = 1 / 0 = 0`.  LType u_5] [AlgebraAlgebra.{u, v} (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] : Type (max u v)An associative unital `R`-algebra is a semiring `A` equipped with a map into its center `R → A`.

See the implementation notes in this file for discussion of the details of this definition.
 (HasQuotient.Quotient.{u, v} (A : outParam (Type u)) {B : Type v} [self : HasQuotient A B] : B → Type (max u v)`HasQuotient.Quotient A b` (denoted as `A ⧸ b`) is the quotient of the type `A` by `b`.

This differs from `HasQuotient.quotient'` in that the `A` argument is explicit,
which is necessary to make Lean show the notation in the goal state.
AType u_1 ⧸HasQuotient.Quotient.{u, v} (A : outParam (Type u)) {B : Type v} [self : HasQuotient A B] : B → Type (max u v)`HasQuotient.Quotient A b` (denoted as `A ⧸ b`) is the quotient of the type `A` by `b`.

This differs from `HasQuotient.quotient'` in that the `A` argument is explicit,
which is necessary to make Lean show the notation in the goal state.
 PIdeal A)HasQuotient.Quotient.{u, v} (A : outParam (Type u)) {B : Type v} [self : HasQuotient A B] : B → Type (max u v)`HasQuotient.Quotient A b` (denoted as `A ⧸ b`) is the quotient of the type `A` by `b`.

This differs from `HasQuotient.quotient'` in that the `A` argument is explicit,
which is necessary to make Lean show the notation in the goal state.
 KType u_4]
  [AlgebraAlgebra.{u, v} (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] : Type (max u v)An associative unital `R`-algebra is a semiring `A` equipped with a map into its center `R → A`.

See the implementation notes in this file for discussion of the details of this definition.
 (HasQuotient.Quotient.{u, v} (A : outParam (Type u)) {B : Type v} [self : HasQuotient A B] : B → Type (max u v)`HasQuotient.Quotient A b` (denoted as `A ⧸ b`) is the quotient of the type `A` by `b`.

This differs from `HasQuotient.quotient'` in that the `A` argument is explicit,
which is necessary to make Lean show the notation in the goal state.
BType u_2 ⧸HasQuotient.Quotient.{u, v} (A : outParam (Type u)) {B : Type v} [self : HasQuotient A B] : B → Type (max u v)`HasQuotient.Quotient A b` (denoted as `A ⧸ b`) is the quotient of the type `A` by `b`.

This differs from `HasQuotient.quotient'` in that the `A` argument is explicit,
which is necessary to make Lean show the notation in the goal state.
 QIdeal B)HasQuotient.Quotient.{u, v} (A : outParam (Type u)) {B : Type v} [self : HasQuotient A B] : B → Type (max u v)`HasQuotient.Quotient A b` (denoted as `A ⧸ b`) is the quotient of the type `A` by `b`.

This differs from `HasQuotient.quotient'` in that the `A` argument is explicit,
which is necessary to make Lean show the notation in the goal state.
 LType u_5] [AlgebraAlgebra.{u, v} (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] : Type (max u v)An associative unital `R`-algebra is a semiring `A` equipped with a map into its center `R → A`.

See the implementation notes in this file for discussion of the details of this definition.
 (HasQuotient.Quotient.{u, v} (A : outParam (Type u)) {B : Type v} [self : HasQuotient A B] : B → Type (max u v)`HasQuotient.Quotient A b` (denoted as `A ⧸ b`) is the quotient of the type `A` by `b`.

This differs from `HasQuotient.quotient'` in that the `A` argument is explicit,
which is necessary to make Lean show the notation in the goal state.
AType u_1 ⧸HasQuotient.Quotient.{u, v} (A : outParam (Type u)) {B : Type v} [self : HasQuotient A B] : B → Type (max u v)`HasQuotient.Quotient A b` (denoted as `A ⧸ b`) is the quotient of the type `A` by `b`.

This differs from `HasQuotient.quotient'` in that the `A` argument is explicit,
which is necessary to make Lean show the notation in the goal state.
 PIdeal A)HasQuotient.Quotient.{u, v} (A : outParam (Type u)) {B : Type v} [self : HasQuotient A B] : B → Type (max u v)`HasQuotient.Quotient A b` (denoted as `A ⧸ b`) is the quotient of the type `A` by `b`.

This differs from `HasQuotient.quotient'` in that the `A` argument is explicit,
which is necessary to make Lean show the notation in the goal state.
 LType u_5]
  [IsScalarTowerIsScalarTower.{u_9, u_10, u_11} (M : Type u_9) (N : Type u_10) (α : Type u_11) [SMul M N] [SMul N α] [SMul M α] : PropAn instance of `IsScalarTower M N α` states that the multiplicative
action of `M` on `α` is determined by the multiplicative actions of `M` on `N`
and `N` on `α`.  (HasQuotient.Quotient.{u, v} (A : outParam (Type u)) {B : Type v} [self : HasQuotient A B] : B → Type (max u v)`HasQuotient.Quotient A b` (denoted as `A ⧸ b`) is the quotient of the type `A` by `b`.

This differs from `HasQuotient.quotient'` in that the `A` argument is explicit,
which is necessary to make Lean show the notation in the goal state.
AType u_1 ⧸HasQuotient.Quotient.{u, v} (A : outParam (Type u)) {B : Type v} [self : HasQuotient A B] : B → Type (max u v)`HasQuotient.Quotient A b` (denoted as `A ⧸ b`) is the quotient of the type `A` by `b`.

This differs from `HasQuotient.quotient'` in that the `A` argument is explicit,
which is necessary to make Lean show the notation in the goal state.
 PIdeal A)HasQuotient.Quotient.{u, v} (A : outParam (Type u)) {B : Type v} [self : HasQuotient A B] : B → Type (max u v)`HasQuotient.Quotient A b` (denoted as `A ⧸ b`) is the quotient of the type `A` by `b`.

This differs from `HasQuotient.quotient'` in that the `A` argument is explicit,
which is necessary to make Lean show the notation in the goal state.
 (HasQuotient.Quotient.{u, v} (A : outParam (Type u)) {B : Type v} [self : HasQuotient A B] : B → Type (max u v)`HasQuotient.Quotient A b` (denoted as `A ⧸ b`) is the quotient of the type `A` by `b`.

This differs from `HasQuotient.quotient'` in that the `A` argument is explicit,
which is necessary to make Lean show the notation in the goal state.
BType u_2 ⧸HasQuotient.Quotient.{u, v} (A : outParam (Type u)) {B : Type v} [self : HasQuotient A B] : B → Type (max u v)`HasQuotient.Quotient A b` (denoted as `A ⧸ b`) is the quotient of the type `A` by `b`.

This differs from `HasQuotient.quotient'` in that the `A` argument is explicit,
which is necessary to make Lean show the notation in the goal state.
 QIdeal B)HasQuotient.Quotient.{u, v} (A : outParam (Type u)) {B : Type v} [self : HasQuotient A B] : B → Type (max u v)`HasQuotient.Quotient A b` (denoted as `A ⧸ b`) is the quotient of the type `A` by `b`.

This differs from `HasQuotient.quotient'` in that the `A` argument is explicit,
which is necessary to make Lean show the notation in the goal state.
 LType u_5]
  [AlgebraAlgebra.{u, v} (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] : Type (max u v)An associative unital `R`-algebra is a semiring `A` equipped with a map into its center `R → A`.

See the implementation notes in this file for discussion of the details of this definition.
 KType u_4 LType u_5]
  [IsScalarTowerIsScalarTower.{u_9, u_10, u_11} (M : Type u_9) (N : Type u_10) (α : Type u_11) [SMul M N] [SMul N α] [SMul M α] : PropAn instance of `IsScalarTower M N α` states that the multiplicative
action of `M` on `α` is determined by the multiplicative actions of `M` on `N`
and `N` on `α`.  (HasQuotient.Quotient.{u, v} (A : outParam (Type u)) {B : Type v} [self : HasQuotient A B] : B → Type (max u v)`HasQuotient.Quotient A b` (denoted as `A ⧸ b`) is the quotient of the type `A` by `b`.

This differs from `HasQuotient.quotient'` in that the `A` argument is explicit,
which is necessary to make Lean show the notation in the goal state.
AType u_1 ⧸HasQuotient.Quotient.{u, v} (A : outParam (Type u)) {B : Type v} [self : HasQuotient A B] : B → Type (max u v)`HasQuotient.Quotient A b` (denoted as `A ⧸ b`) is the quotient of the type `A` by `b`.

This differs from `HasQuotient.quotient'` in that the `A` argument is explicit,
which is necessary to make Lean show the notation in the goal state.
 PIdeal A)HasQuotient.Quotient.{u, v} (A : outParam (Type u)) {B : Type v} [self : HasQuotient A B] : B → Type (max u v)`HasQuotient.Quotient A b` (denoted as `A ⧸ b`) is the quotient of the type `A` by `b`.

This differs from `HasQuotient.quotient'` in that the `A` argument is explicit,
which is necessary to make Lean show the notation in the goal state.
 KType u_4 LType u_5]
  [Algebra.IsInvariantAlgebra.IsInvariant.{u_1, u_2, u_3} (A : Type u_1) (B : Type u_2) (G : Type u_3) [CommSemiring A] [Semiring B]
  [Algebra A B] [Group G] [MulSemiringAction G B] : PropAn action of a group `G` on an extension of rings `B/A` is invariant if every fixed point of
`B` lies in the image of `A`. The converse statement that every point in the image of `A` is fixed
by `G` is `smul_algebraMap` (assuming `SMulCommClass A B G`).  AType u_1 BType u_2 GType u_3]
  [IsFractionRingIsFractionRing.{u_6, u_7} (R : Type u_6) [CommSemiring R] (K : Type u_7) [CommSemiring K] [Algebra R K] : Prop`IsFractionRing R K` states `K` is the ring of fractions of a commutative ring `R`.  (HasQuotient.Quotient.{u, v} (A : outParam (Type u)) {B : Type v} [self : HasQuotient A B] : B → Type (max u v)`HasQuotient.Quotient A b` (denoted as `A ⧸ b`) is the quotient of the type `A` by `b`.

This differs from `HasQuotient.quotient'` in that the `A` argument is explicit,
which is necessary to make Lean show the notation in the goal state.
AType u_1 ⧸HasQuotient.Quotient.{u, v} (A : outParam (Type u)) {B : Type v} [self : HasQuotient A B] : B → Type (max u v)`HasQuotient.Quotient A b` (denoted as `A ⧸ b`) is the quotient of the type `A` by `b`.

This differs from `HasQuotient.quotient'` in that the `A` argument is explicit,
which is necessary to make Lean show the notation in the goal state.
 PIdeal A)HasQuotient.Quotient.{u, v} (A : outParam (Type u)) {B : Type v} [self : HasQuotient A B] : B → Type (max u v)`HasQuotient.Quotient A b` (denoted as `A ⧸ b`) is the quotient of the type `A` by `b`.

This differs from `HasQuotient.quotient'` in that the `A` argument is explicit,
which is necessary to make Lean show the notation in the goal state.
 KType u_4]
  [IsFractionRingIsFractionRing.{u_6, u_7} (R : Type u_6) [CommSemiring R] (K : Type u_7) [CommSemiring K] [Algebra R K] : Prop`IsFractionRing R K` states `K` is the ring of fractions of a commutative ring `R`.  (HasQuotient.Quotient.{u, v} (A : outParam (Type u)) {B : Type v} [self : HasQuotient A B] : B → Type (max u v)`HasQuotient.Quotient A b` (denoted as `A ⧸ b`) is the quotient of the type `A` by `b`.

This differs from `HasQuotient.quotient'` in that the `A` argument is explicit,
which is necessary to make Lean show the notation in the goal state.
BType u_2 ⧸HasQuotient.Quotient.{u, v} (A : outParam (Type u)) {B : Type v} [self : HasQuotient A B] : B → Type (max u v)`HasQuotient.Quotient A b` (denoted as `A ⧸ b`) is the quotient of the type `A` by `b`.

This differs from `HasQuotient.quotient'` in that the `A` argument is explicit,
which is necessary to make Lean show the notation in the goal state.
 QIdeal B)HasQuotient.Quotient.{u, v} (A : outParam (Type u)) {B : Type v} [self : HasQuotient A B] : B → Type (max u v)`HasQuotient.Quotient A b` (denoted as `A ⧸ b`) is the quotient of the type `A` by `b`.

This differs from `HasQuotient.quotient'` in that the `A` argument is explicit,
which is necessary to make Lean show the notation in the goal state.
 LType u_5] :
  Function.SurjectiveFunction.Surjective.{u_1, u_2} {α : Sort u_1} {β : Sort u_2} (f : α → β) : PropA function `f : α → β` is called surjective if every `b : β` is equal to `f a`
for some `a : α`. 
    ⇑(IsFractionRing.stabilizerHomIsFractionRing.stabilizerHom.{u_1, u_2, u_3, u_4, u_5} {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B]
  [Algebra A B] (G : Type u_3) [Group G] [MulSemiringAction G B] [SMulCommClass G A B] (P : Ideal A) (Q : Ideal B)
  [Q.LiesOver P] (K : Type u_4) (L : Type u_5) [Field K] [Field L] [Algebra (A ⧸ P) K] [Algebra (B ⧸ Q) L]
  [Algebra (A ⧸ P) L] [IsScalarTower (A ⧸ P) (B ⧸ Q) L] [Algebra K L] [IsScalarTower (A ⧸ P) K L]
  [IsFractionRing (A ⧸ P) K] [IsFractionRing (B ⧸ Q) L] : ↥(MulAction.stabilizer G Q) →* Gal(L/K)If `Q` lies over `P`, then the stabilizer of `Q` acts on `Frac(B/Q)/Frac(A/P)`.  GType u_3 PIdeal A QIdeal B KType u_4
        LType u_5)

theorem MulSemiringAction.monic_charpoly.{u_2,
    u_3}
  {BType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } (GType u_3 : Type u_3A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. )
  [CommRingCommRing.{u} (α : Type u) : Type uA commutative ring is a ring with commutative multiplication.  BType u_2] [GroupGroup.{u} (G : Type u) : Type uA `Group` is a `Monoid` with an operation `⁻¹` satisfying `a⁻¹ * a = 1`.

There is also a division operation `/` such that `a / b = a * b⁻¹`,
with a default so that `a / b = a * b⁻¹` holds by definition.

Use `Group.ofLeftAxioms` or `Group.ofRightAxioms` to define a group structure
on a type with the minimum proof obligations.
 GType u_3]
  [MulSemiringActionMulSemiringAction.{u, v} (M : Type u) (R : Type v) [Monoid M] [Semiring R] : Type (max u v)Typeclass for multiplicative actions by monoids on semirings.

This combines `DistribMulAction` with `MulDistribMulAction`: it expresses
the interplay between the action and both addition and multiplication on the target.
Two key axioms are `g • (x + y) = (g • x) + (g • y)` and `g • (x * y) = (g • x) * (g • y)`.

A typical use case is the action of a Galois group $Gal(L/K)$ on the field `L`.
 GType u_3 BType u_2] [FintypeFintype.{u_4} (α : Type u_4) : Type u_4`Fintype α` means that `α` is finite, i.e. there are only
finitely many distinct elements of type `α`. The evidence of this
is a finset `elems` (a list up to permutation without duplicates),
together with a proof that everything of type `α` is in the list.  GType u_3]
  (bB : BType u_2) :
  (MulSemiringAction.charpolyMulSemiringAction.charpoly.{u_2, u_3} {B : Type u_2} (G : Type u_3) [CommRing B] [Group G] [MulSemiringAction G B]
  [Fintype G] (b : B) : Polynomial BCharacteristic polynomial of a finite group action on a ring.  GType u_3 bB).MonicPolynomial.Monic.{u} {R : Type u} [Semiring R] (p : Polynomial R) : Propa polynomial is `Monic` if its leading coefficient is 1 

theorem Algebra.IsInvariant.charpoly_mem_lifts.{u_1,
    u_2, u_3}
  (AType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) (BType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. )
  (GType u_3 : Type u_3A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) [CommRingCommRing.{u} (α : Type u) : Type uA commutative ring is a ring with commutative multiplication.  AType u_1] [CommRingCommRing.{u} (α : Type u) : Type uA commutative ring is a ring with commutative multiplication.  BType u_2]
  [AlgebraAlgebra.{u, v} (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] : Type (max u v)An associative unital `R`-algebra is a semiring `A` equipped with a map into its center `R → A`.

See the implementation notes in this file for discussion of the details of this definition.
 AType u_1 BType u_2] [GroupGroup.{u} (G : Type u) : Type uA `Group` is a `Monoid` with an operation `⁻¹` satisfying `a⁻¹ * a = 1`.

There is also a division operation `/` such that `a / b = a * b⁻¹`,
with a default so that `a / b = a * b⁻¹` holds by definition.

Use `Group.ofLeftAxioms` or `Group.ofRightAxioms` to define a group structure
on a type with the minimum proof obligations.
 GType u_3]
  [MulSemiringActionMulSemiringAction.{u, v} (M : Type u) (R : Type v) [Monoid M] [Semiring R] : Type (max u v)Typeclass for multiplicative actions by monoids on semirings.

This combines `DistribMulAction` with `MulDistribMulAction`: it expresses
the interplay between the action and both addition and multiplication on the target.
Two key axioms are `g • (x + y) = (g • x) + (g • y)` and `g • (x * y) = (g • x) * (g • y)`.

A typical use case is the action of a Galois group $Gal(L/K)$ on the field `L`.
 GType u_3 BType u_2]
  [Algebra.IsInvariantAlgebra.IsInvariant.{u_1, u_2, u_3} (A : Type u_1) (B : Type u_2) (G : Type u_3) [CommSemiring A] [Semiring B]
  [Algebra A B] [Group G] [MulSemiringAction G B] : PropAn action of a group `G` on an extension of rings `B/A` is invariant if every fixed point of
`B` lies in the image of `A`. The converse statement that every point in the image of `A` is fixed
by `G` is `smul_algebraMap` (assuming `SMulCommClass A B G`).  AType u_1 BType u_2 GType u_3] [FintypeFintype.{u_4} (α : Type u_4) : Type u_4`Fintype α` means that `α` is finite, i.e. there are only
finitely many distinct elements of type `α`. The evidence of this
is a finset `elems` (a list up to permutation without duplicates),
together with a proof that everything of type `α` is in the list.  GType u_3]
  (bB : BType u_2) :
  MulSemiringAction.charpolyMulSemiringAction.charpoly.{u_2, u_3} {B : Type u_2} (G : Type u_3) [CommRing B] [Group G] [MulSemiringAction G B]
  [Fintype G] (b : B) : Polynomial BCharacteristic polynomial of a finite group action on a ring.  GType u_3 bB ∈Membership.mem.{u, v} {α : outParam (Type u)} {γ : Type v} [self : Membership α γ] : γ → α → PropThe membership relation `a ∈ s : Prop` where `a : α`, `s : γ`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∈` in identifiers is `mem`.
    Polynomial.liftsPolynomial.lifts.{u, v} {R : Type u} [Semiring R] {S : Type v} [Semiring S] (f : R →+* S) : Subsemiring (Polynomial S)We define the subsemiring of polynomials that lifts as the image of `RingHom.of (map f)`.  (algebraMapalgebraMap.{u, v} (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] [Algebra R A] : R →+* AEmbedding `R →+* A` given by `Algebra` structure.  AType u_1 BType u_2)

theorem Algebra.IsInvariant.isIntegral.{u_1, u_2,
    u_3}
  (AType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) (BType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. )
  (GType u_3 : Type u_3A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) [CommRingCommRing.{u} (α : Type u) : Type uA commutative ring is a ring with commutative multiplication.  AType u_1] [CommRingCommRing.{u} (α : Type u) : Type uA commutative ring is a ring with commutative multiplication.  BType u_2]
  [AlgebraAlgebra.{u, v} (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] : Type (max u v)An associative unital `R`-algebra is a semiring `A` equipped with a map into its center `R → A`.

See the implementation notes in this file for discussion of the details of this definition.
 AType u_1 BType u_2] [GroupGroup.{u} (G : Type u) : Type uA `Group` is a `Monoid` with an operation `⁻¹` satisfying `a⁻¹ * a = 1`.

There is also a division operation `/` such that `a / b = a * b⁻¹`,
with a default so that `a / b = a * b⁻¹` holds by definition.

Use `Group.ofLeftAxioms` or `Group.ofRightAxioms` to define a group structure
on a type with the minimum proof obligations.
 GType u_3]
  [MulSemiringActionMulSemiringAction.{u, v} (M : Type u) (R : Type v) [Monoid M] [Semiring R] : Type (max u v)Typeclass for multiplicative actions by monoids on semirings.

This combines `DistribMulAction` with `MulDistribMulAction`: it expresses
the interplay between the action and both addition and multiplication on the target.
Two key axioms are `g • (x + y) = (g • x) + (g • y)` and `g • (x * y) = (g • x) * (g • y)`.

A typical use case is the action of a Galois group $Gal(L/K)$ on the field `L`.
 GType u_3 BType u_2]
  [Algebra.IsInvariantAlgebra.IsInvariant.{u_1, u_2, u_3} (A : Type u_1) (B : Type u_2) (G : Type u_3) [CommSemiring A] [Semiring B]
  [Algebra A B] [Group G] [MulSemiringAction G B] : PropAn action of a group `G` on an extension of rings `B/A` is invariant if every fixed point of
`B` lies in the image of `A`. The converse statement that every point in the image of `A` is fixed
by `G` is `smul_algebraMap` (assuming `SMulCommClass A B G`).  AType u_1 BType u_2 GType u_3] [FiniteFinite.{u_3} (α : Sort u_3) : PropA type is `Finite` if it is in bijective correspondence to some `Fin n`.

This is similar to `Fintype`, but `Finite` is a proposition rather than data.
A particular benefit to this is that `Finite` instances are definitionally equal to one another
(due to proof irrelevance) rather than being merely propositionally equal,
and, furthermore, `Finite` instances generally avoid the need for `Decidable` instances.
One other notable difference is that `Finite` allows there to be `Finite p` instances
for all `p : Prop`, which is not allowed by `Fintype` due to universe constraints.
An application of this is that `Finite (x ∈ s → β x)` follows from the general instance for pi
types, assuming `[∀ x, Finite (β x)]`.
Implementation note: this is a reason `Finite α` is not defined as `Nonempty (Fintype α)`.

Every `Fintype` instance provides a `Finite` instance via `Finite.of_fintype`.
Conversely, one can noncomputably create a `Fintype` instance from a `Finite` instance
via `Fintype.ofFinite`. In a proof one might write
```lean
  have := Fintype.ofFinite α
```
to obtain such an instance.

Do not write noncomputable `Fintype` instances; instead write `Finite` instances
and use this `Fintype.ofFinite` interface.
The `Fintype` instances should be relied upon to be computable for evaluation purposes.

Theorems should use `Finite` instead of `Fintype`, unless definitions in the theorem statement
require `Fintype`.
Definitions should prefer `Finite` as well, unless it is important that the definitions
are meant to be computable in the reduction or `#eval` sense.
 GType u_3] :
  Algebra.IsIntegralAlgebra.IsIntegral.{u_1, u_3} (R : Type u_1) (A : Type u_3) [CommRing R] [Ring A] [Algebra R A] : PropAn algebra is integral if every element of the extension is integral over the base ring.  AType u_1 BType u_2

theorem FixedPoints.toAlgAut_surjective.{u_2, u_3}
  (GType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) (FType u_3 : Type u_3A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) [GroupGroup.{u} (G : Type u) : Type uA `Group` is a `Monoid` with an operation `⁻¹` satisfying `a⁻¹ * a = 1`.

There is also a division operation `/` such that `a / b = a * b⁻¹`,
with a default so that `a / b = a * b⁻¹` holds by definition.

Use `Group.ofLeftAxioms` or `Group.ofRightAxioms` to define a group structure
on a type with the minimum proof obligations.
 GType u_2]
  [FieldField.{u} (K : Type u) : Type uA `Field` is a `CommRing` with multiplicative inverses for nonzero elements.

An instance of `Field K` includes maps `ratCast : ℚ → K` and `qsmul : ℚ → K → K`.
Those two fields are needed to implement the `DivisionRing K → Algebra ℚ K` instance since we need
to control the specific definitions for some special cases of `K` (in particular `K = ℚ` itself).
See also note [forgetful inheritance].

If the field has positive characteristic `p`, our division by zero convention forces
`ratCast (1 / p) = 1 / 0 = 0`.  FType u_3] [MulSemiringActionMulSemiringAction.{u, v} (M : Type u) (R : Type v) [Monoid M] [Semiring R] : Type (max u v)Typeclass for multiplicative actions by monoids on semirings.

This combines `DistribMulAction` with `MulDistribMulAction`: it expresses
the interplay between the action and both addition and multiplication on the target.
Two key axioms are `g • (x + y) = (g • x) + (g • y)` and `g • (x * y) = (g • x) * (g • y)`.

A typical use case is the action of a Galois group $Gal(L/K)$ on the field `L`.
 GType u_2 FType u_3]
  [FiniteFinite.{u_3} (α : Sort u_3) : PropA type is `Finite` if it is in bijective correspondence to some `Fin n`.

This is similar to `Fintype`, but `Finite` is a proposition rather than data.
A particular benefit to this is that `Finite` instances are definitionally equal to one another
(due to proof irrelevance) rather than being merely propositionally equal,
and, furthermore, `Finite` instances generally avoid the need for `Decidable` instances.
One other notable difference is that `Finite` allows there to be `Finite p` instances
for all `p : Prop`, which is not allowed by `Fintype` due to universe constraints.
An application of this is that `Finite (x ∈ s → β x)` follows from the general instance for pi
types, assuming `[∀ x, Finite (β x)]`.
Implementation note: this is a reason `Finite α` is not defined as `Nonempty (Fintype α)`.

Every `Fintype` instance provides a `Finite` instance via `Finite.of_fintype`.
Conversely, one can noncomputably create a `Fintype` instance from a `Finite` instance
via `Fintype.ofFinite`. In a proof one might write
```lean
  have := Fintype.ofFinite α
```
to obtain such an instance.

Do not write noncomputable `Fintype` instances; instead write `Finite` instances
and use this `Fintype.ofFinite` interface.
The `Fintype` instances should be relied upon to be computable for evaluation purposes.

Theorems should use `Finite` instead of `Fintype`, unless definitions in the theorem statement
require `Fintype`.
Definitions should prefer `Finite` as well, unless it is important that the definitions
are meant to be computable in the reduction or `#eval` sense.
 GType u_2] :
  Function.SurjectiveFunction.Surjective.{u_1, u_2} {α : Sort u_1} {β : Sort u_2} (f : α → β) : PropA function `f : α → β` is called surjective if every `b : β` is equal to `f a`
for some `a : α`. 
    ⇑(MulSemiringAction.toAlgAutMulSemiringAction.toAlgAut.{u_2, u_3, u_4} (G : Type u_2) (R : Type u_3) (A : Type u_4) [CommSemiring R] [Semiring A]
  [Algebra R A] [Group G] [MulSemiringAction G A] [SMulCommClass G R A] : G →* A ≃ₐ[R] AEach element of the group defines an algebra equivalence.

This is a stronger version of `MulSemiringAction.toRingAut` and
`DistribMulAction.toModuleEnd`.  GType u_2
        (↥(FixedPoints.subfieldFixedPoints.subfield.{u, v} (M : Type u) [Monoid M] (F : Type v) [Field F] [MulSemiringAction M F] : Subfield FThe subfield of fixed points by a monoid action.  GType u_2 FType u_3)) FType u_3)

theorem IsAlgebraic.exists_smul_eq_mul.{u_1, u_2}
  {RType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } {SType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  [CommRingCommRing.{u} (α : Type u) : Type uA commutative ring is a ring with commutative multiplication.  RType u_1] [RingRing.{u} (R : Type u) : Type uA `Ring` is a `Semiring` with negation making it an additive group.  SType u_2] [AlgebraAlgebra.{u, v} (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] : Type (max u v)An associative unital `R`-algebra is a semiring `A` equipped with a map into its center `R → A`.

See the implementation notes in this file for discussion of the details of this definition.
 RType u_1 SType u_2]
  (aS : SType u_2) {bS : SType u_2} (hRbIsAlgebraic R b : IsAlgebraicIsAlgebraic.{u, v} (R : Type u) {A : Type v} [CommRing R] [Ring A] [Algebra R A] (x : A) : PropAn element of an R-algebra is algebraic over R if it is a root of a nonzero polynomial
with coefficients in R.  RType u_1 bS)
  (hbb ∈ nonZeroDivisors S : bS ∈Membership.mem.{u, v} {α : outParam (Type u)} {γ : Type v} [self : Membership α γ] : γ → α → PropThe membership relation `a ∈ s : Prop` where `a : α`, `s : γ`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∈` in identifiers is `mem`. nonZeroDivisorsnonZeroDivisors.{u_1} (M₀ : Type u_1) [MonoidWithZero M₀] : Submonoid M₀The submonoid of non-zero-divisors of a `MonoidWithZero` `M₀`.  SType u_2) :
  ∃ cS dR, dR ≠Ne.{u} {α : Sort u} (a b : α) : Prop`a ≠ b`, or `Ne a b` is defined as `¬ (a = b)` or `a = b → False`,
and asserts that `a` and `b` are not equal.


Conventions for notations in identifiers:

 * The recommended spelling of `≠` in identifiers is `ne`. 0 ∧And (a b : Prop) : Prop`And a b`, or `a ∧ b`, is the conjunction of propositions. It can be
constructed and destructed like a pair: if `ha : a` and `hb : b` then
`⟨ha, hb⟩ : a ∧ b`, and if `h : a ∧ b` then `h.left : a` and `h.right : b`.


Conventions for notations in identifiers:

 * The recommended spelling of `∧` in identifiers is `and`.

 * The recommended spelling of `/\` in identifiers is `and` (prefer `∧` over `/\`). dR •HSMul.hSMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HSMul α β γ] : α → β → γ`a • b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent, but it is intended to be used for left actions. 

Conventions for notations in identifiers:

 * The recommended spelling of `•` in identifiers is `smul`. aS =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`. bS *HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `*` in identifiers is `mul`. cS