Documentation

Mathlib.FieldTheory.Relrank

Relative rank of subfields and intermediate fields #

This file contains basics about the relative rank of subfields and intermediate fields.

Main definitions #

source
noncomputable def Subfield.relrank {E : Type v} [Field E] (A B : Subfield E) :
Cardinal.{v}

Subfield.relrank A B is defined to be [B : A ⊓ B] as a Cardinal, in particular, when A ≤ B it is [B : A], the degree of the field extension B / A. This is similar to Subgroup.relindex but it is Cardinal valued.

Equations
Instances For
    source
    noncomputable def Subfield.relfinrank {E : Type v} [Field E] (A B : Subfield E) :
    ℕ

    The Nat version of Subfield.relrank. If B / A ⊓ B is an infinite extension, then it is zero.

    Equations
    Instances For
      source
      theorem Subfield.relfinrank_eq_toNat_relrank {E : Type v} [Field E] (A B : Subfield E) :
      A.relfinrank B = Cardinal.toNat (A.relrank B)
      source
      theorem Subfield.relrank_eq_of_inf_eq {E : Type v} [Field E] {A B C : Subfield E} (h : A ⊓ C = B ⊓ C) :
      A.relrank C = B.relrank C
      source
      theorem Subfield.relfinrank_eq_of_inf_eq {E : Type v} [Field E] {A B C : Subfield E} (h : A ⊓ C = B ⊓ C) :
      A.relfinrank C = B.relfinrank C
      source
      theorem Subfield.relrank_eq_rank_of_le {E : Type v} [Field E] {A B : Subfield E} (h : A ≤ B) :
      A.relrank B = Module.rank ↥A ↥(Subfield.extendScalars h)

      If A ≤ B, then Subfield.relrank A B is [B : A]

      source
      theorem Subfield.relfinrank_eq_finrank_of_le {E : Type v} [Field E] {A B : Subfield E} (h : A ≤ B) :
      A.relfinrank B = Module.finrank ↥A ↥(Subfield.extendScalars h)

      If A ≤ B, then Subfield.relfinrank A B is [B : A]

      source
      theorem Subfield.inf_relrank_right {E : Type v} [Field E] (A B : Subfield E) :
      (A ⊓ B).relrank B = A.relrank B
      source
      theorem Subfield.inf_relfinrank_right {E : Type v} [Field E] (A B : Subfield E) :
      (A ⊓ B).relfinrank B = A.relfinrank B
      source
      theorem Subfield.inf_relrank_left {E : Type v} [Field E] (A B : Subfield E) :
      (A ⊓ B).relrank A = B.relrank A
      source
      theorem Subfield.inf_relfinrank_left {E : Type v} [Field E] (A B : Subfield E) :
      (A ⊓ B).relfinrank A = B.relfinrank A
      source
      @[simp]
      theorem Subfield.relrank_self {E : Type v} [Field E] (A : Subfield E) :
      A.relrank A = 1
      source
      @[simp]
      theorem Subfield.relfinrank_self {E : Type v} [Field E] (A : Subfield E) :
      A.relfinrank A = 1
      source
      theorem Subfield.relrank_eq_one_of_le {E : Type v} [Field E] {A B : Subfield E} (h : B ≤ A) :
      A.relrank B = 1
      source
      theorem Subfield.relfinrank_eq_one_of_le {E : Type v} [Field E] {A B : Subfield E} (h : B ≤ A) :
      A.relfinrank B = 1
      source
      theorem Subfield.relrank_mul_rank_top {E : Type v} [Field E] {A B : Subfield E} (h : A ≤ B) :
      A.relrank B * Module.rank (↥B) E = Module.rank (↥A) E
      source
      theorem Subfield.relfinrank_mul_finrank_top {E : Type v} [Field E] {A B : Subfield E} (h : A ≤ B) :
      A.relfinrank B * Module.finrank (↥B) E = Module.finrank (↥A) E
      source
      @[simp]
      theorem Subfield.relrank_top_left {E : Type v} [Field E] (A : Subfield E) :
      ⊤.relrank A = 1
      source
      @[simp]
      theorem Subfield.relfinrank_top_left {E : Type v} [Field E] (A : Subfield E) :
      ⊤.relfinrank A = 1
      source
      @[simp]
      theorem Subfield.relrank_top_right {E : Type v} [Field E] (A : Subfield E) :
      A.relrank ⊤ = Module.rank (↥A) E
      source
      @[simp]
      theorem Subfield.relfinrank_top_right {E : Type v} [Field E] (A : Subfield E) :
      A.relfinrank ⊤ = Module.finrank (↥A) E
      source
      theorem Subfield.lift_relrank_map_map {E : Type v} [Field E] {L : Type w} [Field L] (A B : Subfield E) (f : E →+* L) :
      Cardinal.lift.{v, w} ((Subfield.map f A).relrank (Subfield.map f B)) = Cardinal.lift.{w, v} (A.relrank B)
      source
      theorem Subfield.relrank_map_map {E : Type v} [Field E] (A B : Subfield E) {L : Type v} [Field L] (f : E →+* L) :
      (Subfield.map f A).relrank (Subfield.map f B) = A.relrank B
      source
      theorem Subfield.lift_relrank_comap {E : Type v} [Field E] {L : Type w} [Field L] (A : Subfield E) (f : L →+* E) (B : Subfield L) :
      Cardinal.lift.{v, w} ((Subfield.comap f A).relrank B) = Cardinal.lift.{w, v} (A.relrank (Subfield.map f B))
      source
      theorem Subfield.relrank_comap {E : Type v} [Field E] (A : Subfield E) {L : Type v} [Field L] (f : L →+* E) (B : Subfield L) :
      (Subfield.comap f A).relrank B = A.relrank (Subfield.map f B)
      source
      theorem Subfield.relfinrank_comap {E : Type v} [Field E] {L : Type w} [Field L] (A : Subfield E) (f : L →+* E) (B : Subfield L) :
      (Subfield.comap f A).relfinrank B = A.relfinrank (Subfield.map f B)
      source
      theorem Subfield.lift_rank_comap {E : Type v} [Field E] {L : Type w} [Field L] (A : Subfield E) (f : L →+* E) :
      Cardinal.lift.{v, w} (Module.rank (↥(Subfield.comap f A)) L) = Cardinal.lift.{w, v} (A.relrank f.fieldRange)
      source
      theorem Subfield.rank_comap {E : Type v} [Field E] (A : Subfield E) {L : Type v} [Field L] (f : L →+* E) :
      Module.rank (↥(Subfield.comap f A)) L = A.relrank f.fieldRange
      source
      theorem Subfield.finrank_comap {E : Type v} [Field E] {L : Type w} [Field L] (A : Subfield E) (f : L →+* E) :
      Module.finrank (↥(Subfield.comap f A)) L = A.relfinrank f.fieldRange
      source
      theorem Subfield.relfinrank_map_map {E : Type v} [Field E] {L : Type w} [Field L] (A B : Subfield E) (f : E →+* L) :
      (Subfield.map f A).relfinrank (Subfield.map f B) = A.relfinrank B
      source
      theorem Subfield.lift_relrank_comap_comap_eq_lift_relrank_inf {E : Type v} [Field E] {L : Type w} [Field L] (A B : Subfield E) (f : L →+* E) :
      Cardinal.lift.{v, w} ((Subfield.comap f A).relrank (Subfield.comap f B)) = Cardinal.lift.{w, v} (A.relrank (B ⊓ f.fieldRange))
      source
      theorem Subfield.relrank_comap_comap_eq_relrank_inf {E : Type v} [Field E] (A B : Subfield E) {L : Type v} [Field L] (f : L →+* E) :
      (Subfield.comap f A).relrank (Subfield.comap f B) = A.relrank (B ⊓ f.fieldRange)
      source
      theorem Subfield.relfinrank_comap_comap_eq_relfinrank_inf {E : Type v} [Field E] {L : Type w} [Field L] (A B : Subfield E) (f : L →+* E) :
      (Subfield.comap f A).relfinrank (Subfield.comap f B) = A.relfinrank (B ⊓ f.fieldRange)
      source
      theorem Subfield.lift_relrank_comap_comap_eq_lift_relrank_of_le {E : Type v} [Field E] {L : Type w} [Field L] (A B : Subfield E) (f : L →+* E) (h : B ≤ f.fieldRange) :
      Cardinal.lift.{v, w} ((Subfield.comap f A).relrank (Subfield.comap f B)) = Cardinal.lift.{w, v} (A.relrank B)
      source
      theorem Subfield.relrank_comap_comap_eq_relrank_of_le {E : Type v} [Field E] (A B : Subfield E) {L : Type v} [Field L] (f : L →+* E) (h : B ≤ f.fieldRange) :
      (Subfield.comap f A).relrank (Subfield.comap f B) = A.relrank B
      source
      theorem Subfield.relfinrank_comap_comap_eq_relfinrank_of_le {E : Type v} [Field E] {L : Type w} [Field L] (A B : Subfield E) (f : L →+* E) (h : B ≤ f.fieldRange) :
      (Subfield.comap f A).relfinrank (Subfield.comap f B) = A.relfinrank B
      source
      theorem Subfield.lift_relrank_comap_comap_eq_lift_relrank_of_surjective {E : Type v} [Field E] {L : Type w} [Field L] (A B : Subfield E) (f : L →+* E) (h : Function.Surjective ⇑f) :
      Cardinal.lift.{v, w} ((Subfield.comap f A).relrank (Subfield.comap f B)) = Cardinal.lift.{w, v} (A.relrank B)
      source
      theorem Subfield.relrank_comap_comap_eq_relrank_of_surjective {E : Type v} [Field E] (A B : Subfield E) {L : Type v} [Field L] (f : L →+* E) (h : Function.Surjective ⇑f) :
      (Subfield.comap f A).relrank (Subfield.comap f B) = A.relrank B
      source
      theorem Subfield.relfinrank_comap_comap_eq_relfinrank_of_surjective {E : Type v} [Field E] {L : Type w} [Field L] (A B : Subfield E) (f : L →+* E) (h : Function.Surjective ⇑f) :
      (Subfield.comap f A).relfinrank (Subfield.comap f B) = A.relfinrank B
      source
      theorem Subfield.relrank_dvd_rank_top_of_le {E : Type v} [Field E] {A B : Subfield E} (h : A ≤ B) :
      A.relrank B ∣ Module.rank (↥A) E
      source
      theorem Subfield.relfinrank_dvd_finrank_top_of_le {E : Type v} [Field E] {A B : Subfield E} (h : A ≤ B) :
      A.relfinrank B ∣ Module.finrank (↥A) E
      source
      theorem Subfield.relrank_mul_relrank {E : Type v} [Field E] {A B C : Subfield E} (h1 : A ≤ B) (h2 : B ≤ C) :
      A.relrank B * B.relrank C = A.relrank C
      source
      theorem Subfield.relfinrank_mul_relfinrank {E : Type v} [Field E] {A B C : Subfield E} (h1 : A ≤ B) (h2 : B ≤ C) :
      A.relfinrank B * B.relfinrank C = A.relfinrank C
      source
      theorem Subfield.relrank_inf_mul_relrank {E : Type v} [Field E] (A B C : Subfield E) :
      A.relrank (B ⊓ C) * B.relrank C = (A ⊓ B).relrank C
      source
      theorem Subfield.relfinrank_inf_mul_relfinrank {E : Type v} [Field E] (A B C : Subfield E) :
      A.relfinrank (B ⊓ C) * B.relfinrank C = (A ⊓ B).relfinrank C
      source
      theorem Subfield.relrank_mul_relrank_eq_inf_relrank {E : Type v} [Field E] (A : Subfield E) {B C : Subfield E} (h : B ≤ C) :
      A.relrank B * B.relrank C = (A ⊓ B).relrank C
      source
      theorem Subfield.relfinrank_mul_relfinrank_eq_inf_relfinrank {E : Type v} [Field E] (A : Subfield E) {B C : Subfield E} (h : B ≤ C) :
      A.relfinrank B * B.relfinrank C = (A ⊓ B).relfinrank C
      source
      theorem Subfield.relrank_inf_mul_relrank_of_le {E : Type v} [Field E] {A B : Subfield E} (C : Subfield E) (h : A ≤ B) :
      A.relrank (B ⊓ C) * B.relrank C = A.relrank C
      source
      theorem Subfield.relfinrank_inf_mul_relfinrank_of_le {E : Type v} [Field E] {A B : Subfield E} (C : Subfield E) (h : A ≤ B) :
      A.relfinrank (B ⊓ C) * B.relfinrank C = A.relfinrank C
      source
      theorem Subfield.relrank_dvd_of_le_left {E : Type v} [Field E] {A B : Subfield E} (C : Subfield E) (h : A ≤ B) :
      B.relrank C ∣ A.relrank C
      source
      theorem Subfield.relfinrank_dvd_of_le_left {E : Type v} [Field E] {A B : Subfield E} (C : Subfield E) (h : A ≤ B) :
      B.relfinrank C ∣ A.relfinrank C
      source
      noncomputable def IntermediateField.relrank {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (A B : IntermediateField F E) :
      Cardinal.{v}

      IntermediateField.relrank A B is defined to be [B : A ⊓ B] as a Cardinal, in particular, when A ≤ B it is [B : A], the degree of the field extension B / A. This is similar to Subgroup.relindex but it is Cardinal valued.

      Equations
      • A.relrank B = A.toSubfield.relrank B.toSubfield
      Instances For
        source
        noncomputable def IntermediateField.relfinrank {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (A B : IntermediateField F E) :
        ℕ

        The Nat version of IntermediateField.relrank. If B / A ⊓ B is an infinite extension, then it is zero.

        Equations
        • A.relfinrank B = A.toSubfield.relfinrank B.toSubfield
        Instances For
          source
          theorem IntermediateField.relfinrank_eq_toNat_relrank {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (A B : IntermediateField F E) :
          A.relfinrank B = Cardinal.toNat (A.relrank B)
          source
          theorem IntermediateField.relrank_eq_of_inf_eq {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {A B C : IntermediateField F E} (h : A ⊓ C = B ⊓ C) :
          A.relrank C = B.relrank C
          source
          theorem IntermediateField.relfinrank_eq_of_inf_eq {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {A B C : IntermediateField F E} (h : A ⊓ C = B ⊓ C) :
          A.relfinrank C = B.relfinrank C
          source
          theorem IntermediateField.relrank_eq_rank_of_le {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {A B : IntermediateField F E} (h : A ≤ B) :
          A.relrank B = Module.rank ↥A ↥(IntermediateField.extendScalars h)

          If A ≤ B, then IntermediateField.relrank A B is [B : A]

          source
          theorem IntermediateField.relfinrank_eq_finrank_of_le {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {A B : IntermediateField F E} (h : A ≤ B) :
          A.relfinrank B = Module.finrank ↥A ↥(IntermediateField.extendScalars h)

          If A ≤ B, then IntermediateField.relrank A B is [B : A]

          source
          theorem IntermediateField.inf_relrank_right {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (A B : IntermediateField F E) :
          (A ⊓ B).relrank B = A.relrank B
          source
          theorem IntermediateField.inf_relfinrank_right {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (A B : IntermediateField F E) :
          (A ⊓ B).relfinrank B = A.relfinrank B
          source
          theorem IntermediateField.inf_relrank_left {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (A B : IntermediateField F E) :
          (A ⊓ B).relrank A = B.relrank A
          source
          theorem IntermediateField.inf_relfinrank_left {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (A B : IntermediateField F E) :
          (A ⊓ B).relfinrank A = B.relfinrank A
          source
          @[simp]
          theorem IntermediateField.relrank_self {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (A : IntermediateField F E) :
          A.relrank A = 1
          source
          @[simp]
          theorem IntermediateField.relfinrank_self {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (A : IntermediateField F E) :
          A.relfinrank A = 1
          source
          theorem IntermediateField.relrank_eq_one_of_le {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {A B : IntermediateField F E} (h : B ≤ A) :
          A.relrank B = 1
          source
          theorem IntermediateField.relfinrank_eq_one_of_le {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {A B : IntermediateField F E} (h : B ≤ A) :
          A.relfinrank B = 1
          source
          theorem IntermediateField.lift_rank_comap {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {L : Type w} [Field L] [Algebra F L] (A : IntermediateField F E) (f : L →ₐ[F] E) :
          Cardinal.lift.{v, w} (Module.rank (↥(IntermediateField.comap f A)) L) = Cardinal.lift.{w, v} (A.relrank f.fieldRange)
          source
          theorem IntermediateField.rank_comap {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (A : IntermediateField F E) {L : Type v} [Field L] [Algebra F L] (f : L →ₐ[F] E) :
          Module.rank (↥(IntermediateField.comap f A)) L = A.relrank f.fieldRange
          source
          theorem IntermediateField.finrank_comap {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {L : Type w} [Field L] [Algebra F L] (A : IntermediateField F E) (f : L →ₐ[F] E) :
          Module.finrank (↥(IntermediateField.comap f A)) L = A.relfinrank f.fieldRange
          source
          theorem IntermediateField.lift_relrank_comap {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {L : Type w} [Field L] [Algebra F L] (A : IntermediateField F E) (f : L →ₐ[F] E) (B : IntermediateField F L) :
          Cardinal.lift.{v, w} ((IntermediateField.comap f A).relrank B) = Cardinal.lift.{w, v} (A.relrank (IntermediateField.map f B))
          source
          theorem IntermediateField.relrank_comap {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (A : IntermediateField F E) {L : Type v} [Field L] [Algebra F L] (f : L →ₐ[F] E) (B : IntermediateField F L) :
          (IntermediateField.comap f A).relrank B = A.relrank (IntermediateField.map f B)
          source
          theorem IntermediateField.relfinrank_comap {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {L : Type w} [Field L] [Algebra F L] (A : IntermediateField F E) (f : L →ₐ[F] E) (B : IntermediateField F L) :
          (IntermediateField.comap f A).relfinrank B = A.relfinrank (IntermediateField.map f B)
          source
          theorem IntermediateField.lift_relrank_map_map {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {L : Type w} [Field L] [Algebra F L] (A B : IntermediateField F E) (f : E →ₐ[F] L) :
          Cardinal.lift.{v, w} ((IntermediateField.map f A).relrank (IntermediateField.map f B)) = Cardinal.lift.{w, v} (A.relrank B)
          source
          theorem IntermediateField.relrank_map_map {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (A B : IntermediateField F E) {L : Type v} [Field L] [Algebra F L] (f : E →ₐ[F] L) :
          (IntermediateField.map f A).relrank (IntermediateField.map f B) = A.relrank B
          source
          theorem IntermediateField.relfinrank_map_map {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {L : Type w} [Field L] [Algebra F L] (A B : IntermediateField F E) (f : E →ₐ[F] L) :
          (IntermediateField.map f A).relfinrank (IntermediateField.map f B) = A.relfinrank B
          source
          theorem IntermediateField.lift_relrank_comap_comap_eq_lift_relrank_inf {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {L : Type w} [Field L] [Algebra F L] (A B : IntermediateField F E) (f : L →ₐ[F] E) :
          Cardinal.lift.{v, w} ((IntermediateField.comap f A).relrank (IntermediateField.comap f B)) = Cardinal.lift.{w, v} (A.relrank (B ⊓ f.fieldRange))
          source
          theorem IntermediateField.relrank_comap_comap_eq_relrank_inf {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (A B : IntermediateField F E) {L : Type v} [Field L] [Algebra F L] (f : L →ₐ[F] E) :
          (IntermediateField.comap f A).relrank (IntermediateField.comap f B) = A.relrank (B ⊓ f.fieldRange)
          source
          theorem IntermediateField.relfinrank_comap_comap_eq_relfinrank_inf {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {L : Type w} [Field L] [Algebra F L] (A B : IntermediateField F E) (f : L →ₐ[F] E) :
          (IntermediateField.comap f A).relfinrank (IntermediateField.comap f B) = A.relfinrank (B ⊓ f.fieldRange)
          source
          theorem IntermediateField.lift_relrank_comap_comap_eq_lift_relrank_of_le {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {L : Type w} [Field L] [Algebra F L] (A B : IntermediateField F E) (f : L →ₐ[F] E) (h : B ≤ f.fieldRange) :
          Cardinal.lift.{v, w} ((IntermediateField.comap f A).relrank (IntermediateField.comap f B)) = Cardinal.lift.{w, v} (A.relrank B)
          source
          theorem IntermediateField.relrank_comap_comap_eq_relrank_of_le {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (A B : IntermediateField F E) {L : Type v} [Field L] [Algebra F L] (f : L →ₐ[F] E) (h : B ≤ f.fieldRange) :
          (IntermediateField.comap f A).relrank (IntermediateField.comap f B) = A.relrank B
          source
          theorem IntermediateField.relfinrank_comap_comap_eq_relfinrank_of_le {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {L : Type w} [Field L] [Algebra F L] (A B : IntermediateField F E) (f : L →ₐ[F] E) (h : B ≤ f.fieldRange) :
          (IntermediateField.comap f A).relfinrank (IntermediateField.comap f B) = A.relfinrank B
          source
          theorem IntermediateField.lift_relrank_comap_comap_eq_lift_relrank_of_surjective {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {L : Type w} [Field L] [Algebra F L] (A B : IntermediateField F E) (f : L →ₐ[F] E) (h : Function.Surjective ⇑f) :
          Cardinal.lift.{v, w} ((IntermediateField.comap f A).relrank (IntermediateField.comap f B)) = Cardinal.lift.{w, v} (A.relrank B)
          source
          theorem IntermediateField.relrank_comap_comap_eq_relrank_of_surjective {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (A B : IntermediateField F E) {L : Type v} [Field L] [Algebra F L] (f : L →ₐ[F] E) (h : Function.Surjective ⇑f) :
          (IntermediateField.comap f A).relrank (IntermediateField.comap f B) = A.relrank B
          source
          theorem IntermediateField.relfinrank_comap_comap_eq_relfinrank_of_surjective {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {L : Type w} [Field L] [Algebra F L] (A B : IntermediateField F E) (f : L →ₐ[F] E) (h : Function.Surjective ⇑f) :
          (IntermediateField.comap f A).relfinrank (IntermediateField.comap f B) = A.relfinrank B
          source
          theorem IntermediateField.relrank_mul_rank_top {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {A B : IntermediateField F E} (h : A ≤ B) :
          A.relrank B * Module.rank (↥B) E = Module.rank (↥A) E
          source
          theorem IntermediateField.relfinrank_mul_finrank_top {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {A B : IntermediateField F E} (h : A ≤ B) :
          A.relfinrank B * Module.finrank (↥B) E = Module.finrank (↥A) E
          source
          theorem IntermediateField.rank_bot_mul_relrank {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {A B : IntermediateField F E} (h : A ≤ B) :
          Module.rank F ↥A * A.relrank B = Module.rank F ↥B
          source
          theorem IntermediateField.finrank_bot_mul_relfinrank {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {A B : IntermediateField F E} (h : A ≤ B) :
          Module.finrank F ↥A * A.relfinrank B = Module.finrank F ↥B
          source
          theorem IntermediateField.relrank_dvd_rank_top_of_le {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {A B : IntermediateField F E} (h : A ≤ B) :
          A.relrank B ∣ Module.rank (↥A) E
          source
          theorem IntermediateField.relfinrank_dvd_finrank_top_of_le {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {A B : IntermediateField F E} (h : A ≤ B) :
          A.relfinrank B ∣ Module.finrank (↥A) E
          source
          theorem IntermediateField.relrank_dvd_rank_bot {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (A B : IntermediateField F E) :
          A.relrank B ∣ Module.rank F ↥B
          source
          theorem IntermediateField.relfinrank_dvd_finrank_bot {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (A B : IntermediateField F E) :
          A.relfinrank B ∣ Module.finrank F ↥B
          source
          theorem IntermediateField.relrank_mul_relrank {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {A B C : IntermediateField F E} (h1 : A ≤ B) (h2 : B ≤ C) :
          A.relrank B * B.relrank C = A.relrank C
          source
          theorem IntermediateField.relfinrank_mul_relfinrank {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {A B C : IntermediateField F E} (h1 : A ≤ B) (h2 : B ≤ C) :
          A.relfinrank B * B.relfinrank C = A.relfinrank C
          source
          theorem IntermediateField.relrank_inf_mul_relrank {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (A B C : IntermediateField F E) :
          A.relrank (B ⊓ C) * B.relrank C = (A ⊓ B).relrank C
          source
          theorem IntermediateField.relfinrank_inf_mul_relfinrank {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (A B C : IntermediateField F E) :
          A.relfinrank (B ⊓ C) * B.relfinrank C = (A ⊓ B).relfinrank C
          source
          theorem IntermediateField.relrank_mul_relrank_eq_inf_relrank {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (A : IntermediateField F E) {B C : IntermediateField F E} (h : B ≤ C) :
          A.relrank B * B.relrank C = (A ⊓ B).relrank C
          source
          theorem IntermediateField.relfinrank_mul_relfinrank_eq_inf_relfinrank {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (A : IntermediateField F E) {B C : IntermediateField F E} (h : B ≤ C) :
          A.relfinrank B * B.relfinrank C = (A ⊓ B).relfinrank C
          source
          theorem IntermediateField.relrank_inf_mul_relrank_of_le {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {A B : IntermediateField F E} (C : IntermediateField F E) (h : A ≤ B) :
          A.relrank (B ⊓ C) * B.relrank C = A.relrank C
          source
          theorem IntermediateField.relfinrank_inf_mul_relfinrank_of_le {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {A B : IntermediateField F E} (C : IntermediateField F E) (h : A ≤ B) :
          A.relfinrank (B ⊓ C) * B.relfinrank C = A.relfinrank C
          source
          @[simp]
          theorem IntermediateField.relrank_top_left {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (A : IntermediateField F E) :
          ⊤.relrank A = 1
          source
          @[simp]
          theorem IntermediateField.relfinrank_top_left {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (A : IntermediateField F E) :
          ⊤.relfinrank A = 1
          source
          @[simp]
          theorem IntermediateField.relrank_top_right {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (A : IntermediateField F E) :
          A.relrank ⊤ = Module.rank (↥A) E
          source
          @[simp]
          theorem IntermediateField.relfinrank_top_right {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (A : IntermediateField F E) :
          A.relfinrank ⊤ = Module.finrank (↥A) E
          source
          @[simp]
          theorem IntermediateField.relrank_bot_left {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (A : IntermediateField F E) :
          ⊥.relrank A = Module.rank F ↥A
          source
          @[simp]
          theorem IntermediateField.relfinrank_bot_left {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (A : IntermediateField F E) :
          ⊥.relfinrank A = Module.finrank F ↥A
          source
          @[simp]
          theorem IntermediateField.relrank_bot_right {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (A : IntermediateField F E) :
          A.relrank ⊥ = 1
          source
          @[simp]
          theorem IntermediateField.relfinrank_bot_right {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (A : IntermediateField F E) :
          A.relfinrank ⊥ = 1
          source
          theorem IntermediateField.relrank_dvd_of_le_left {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {A B : IntermediateField F E} (C : IntermediateField F E) (h : A ≤ B) :
          B.relrank C ∣ A.relrank C
          source
          theorem IntermediateField.relfinrank_dvd_of_le_left {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {A B : IntermediateField F E} (C : IntermediateField F E) (h : A ≤ B) :
          B.relfinrank C ∣ A.relfinrank C