NYLL
Module

AutomorphismTransport.lean

Nyll.ValuedFieldTheory.LocalField.DiscreteValuationField.PrincipalUnits.AutomorphismTransport
17 declarations indexed from sourceView source ↗

Module documentation

Automorphism transport for principal units

A field automorphism preserving the chosen valuation ring acts on the valuation ring, its residue field, its units, and every principal-unit quotient.

Imports2
Imported by4

Declarations

def

valuationSubringRingEquivOfPreserves

L42 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.valuationSubringRingEquivOfPreserves
Documentation

A field automorphism preserving the chosen valuation ring induces a ring automorphism of the valuation ring. This is the unit/residue source used before invoking local reciprocity in the local-field arguments.

Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
open ValuationTheory
open ValuationTheory.DiscreteValuationField.ResidueField
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
Lean source · statement
def valuationSubringRingEquivOfPreserves
    (e : K ≃+* K)
    (hmem :
      ∀ x : K,
        x ∈ F.valuation.valuationSubring ↔
          e x ∈ F.valuation.valuationSubring) :
    F.valuationSubring ≃+* F.valuationSubring
theorem

valuationSubringRingEquivOfPreserves_mem_maximalIdeal_pow_iff

L54 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.valuationSubringRingEquivOfPreserves_mem_maximalIdeal_pow_iff
Documentation

A valuation-ring-preserving field automorphism preserves every power of the maximal ideal of the chosen valuation ring.

Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
open ValuationTheory
open ValuationTheory.DiscreteValuationField.ResidueField
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
Lean source · statement
theorem valuationSubringRingEquivOfPreserves_mem_maximalIdeal_pow_iff
    (e : K ≃+* K)
    (hmem :
      ∀ x : K,
        x ∈ F.valuation.valuationSubring ↔
          e x ∈ F.valuation.valuationSubring)
    (n : ℕ) (x : F.valuationSubring) :
    valuationSubringRingEquivOfPreserves F e hmem x ∈ F.maximalIdeal ^ n ↔
      x ∈ F.maximalIdeal ^ n
def

valuationSubringResidueFieldEquivOfPreserves

L87 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.valuationSubringResidueFieldEquivOfPreserves
Documentation

The residue-field automorphism induced by a field automorphism preserving the chosen valuation ring.

Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
open ValuationTheory
open ValuationTheory.DiscreteValuationField.ResidueField
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
Lean source · statement
def valuationSubringResidueFieldEquivOfPreserves
    (e : K ≃+* K)
    (hmem :
      ∀ x : K,
        x ∈ F.valuation.valuationSubring ↔
          e x ∈ F.valuation.valuationSubring) :
    F.residueField ≃+* F.residueField
theorem

valuationSubringResidueFieldEquivOfPreserves_apply_residue

L104 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.valuationSubringResidueFieldEquivOfPreserves_apply_residue
Documentation

Establishes the identity valuationSubringResidueFieldEquivOfPreserves F e hmem (F.residueMap x) = F.residueMap (valuationSubringRingEquivOfPreserves F e hmem x).

Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
open ValuationTheory
open ValuationTheory.DiscreteValuationField.ResidueField
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
Lean source · statement
theorem valuationSubringResidueFieldEquivOfPreserves_apply_residue
    (e : K ≃+* K)
    (hmem :
      ∀ x : K,
        x ∈ F.valuation.valuationSubring ↔
          e x ∈ F.valuation.valuationSubring)
    (x : F.valuationSubring) :
    valuationSubringResidueFieldEquivOfPreserves F e hmem (F.residueMap x) =
      F.residueMap (valuationSubringRingEquivOfPreserves F e hmem x)
def

valuationSubringUnitEquivOfPreserves

L120 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.valuationSubringUnitEquivOfPreserves
Documentation

The induced automorphism on valuation-ring units.

Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
open ValuationTheory
open ValuationTheory.DiscreteValuationField.ResidueField
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
Lean source · statement
def valuationSubringUnitEquivOfPreserves
    (e : K ≃+* K)
    (hmem :
      ∀ x : K,
        x ∈ F.valuation.valuationSubring ↔
          e x ∈ F.valuation.valuationSubring) :
    F.valuationSubringˣ ≃* F.valuationSubringˣ
theorem

valuationSubringUnitEquivOfPreserves_apply

L135 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.valuationSubringUnitEquivOfPreserves_apply
Documentation

The defining evaluation formula for valuationSubringUnitEquivOfPreserves is ((valuationSubringUnitEquivOfPreserves F e hmem u : F.valuationSubringˣ) : F.valuationSubring) = valuationSubringRingEquivOfPreserves F e hmem (u : F.valuationSubring).

Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
open ValuationTheory
open ValuationTheory.DiscreteValuationField.ResidueField
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
Lean source · statement
theorem valuationSubringUnitEquivOfPreserves_apply
    (e : K ≃+* K)
    (hmem :
      ∀ x : K,
        x ∈ F.valuation.valuationSubring ↔
          e x ∈ F.valuation.valuationSubring)
    (u : F.valuationSubringˣ) :
    ((valuationSubringUnitEquivOfPreserves F e hmem u :
        F.valuationSubringˣ) : F.valuationSubring) =
      valuationSubringRingEquivOfPreserves F e hmem
        (u : F.valuationSubring)
theorem

residueUnitHom_valuationSubringUnitEquivOfPreserves

L150 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.residueUnitHom_valuationSubringUnitEquivOfPreserves
Documentation

Compatibility between the induced unit action and the induced residue-field action.

Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
open ValuationTheory
open ValuationTheory.DiscreteValuationField.ResidueField
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
Lean source · statement
theorem residueUnitHom_valuationSubringUnitEquivOfPreserves
    (e : K ≃+* K)
    (hmem :
      ∀ x : K,
        x ∈ F.valuation.valuationSubring ↔
          e x ∈ F.valuation.valuationSubring)
    (u : F.valuationSubringˣ) :
    higherPrincipalUnitGroup.residueUnitHom F
        (valuationSubringUnitEquivOfPreserves F e hmem u) =
      Units.map
        (valuationSubringResidueFieldEquivOfPreserves F e hmem).toMonoidHom
        (higherPrincipalUnitGroup.residueUnitHom F u)
theorem

valuationSubringUnitEquivOfPreserves_mem_principalUnit_iff

L168 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.valuationSubringUnitEquivOfPreserves_mem_principalUnit_iff
Documentation

The induced automorphism on valuation-ring units preserves every concrete principal-unit level U^n.

Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
open ValuationTheory
open ValuationTheory.DiscreteValuationField.ResidueField
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
Lean source · statement
theorem valuationSubringUnitEquivOfPreserves_mem_principalUnit_iff
    (e : K ≃+* K)
    (hmem :
      ∀ x : K,
        x ∈ F.valuation.valuationSubring ↔
          e x ∈ F.valuation.valuationSubring)
    (n : ℕ) (u : F.valuationSubringˣ) :
    valuationSubringUnitEquivOfPreserves F e hmem u ∈
        higherPrincipalUnitGroup F n ↔
      u ∈ higherPrincipalUnitGroup F n
theorem

higherPrincipalUnitGroup_map_valuationSubringUnitEquivOfPreserves

L191 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.higherPrincipalUnitGroup_map_valuationSubringUnitEquivOfPreserves
Documentation

The subgroup map form of principal-unit preservation for a valuation-ring-preserving field automorphism.

Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
open ValuationTheory
open ValuationTheory.DiscreteValuationField.ResidueField
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
Lean source · statement
theorem higherPrincipalUnitGroup_map_valuationSubringUnitEquivOfPreserves
    (e : K ≃+* K)
    (hmem :
      ∀ x : K,
        x ∈ F.valuation.valuationSubring ↔
          e x ∈ F.valuation.valuationSubring)
    (n : ℕ) :
    (higherPrincipalUnitGroup F n).map
        (valuationSubringUnitEquivOfPreserves F e hmem :
          F.valuationSubringˣ →* F.valuationSubringˣ) =
      higherPrincipalUnitGroup F n
def

unitsModPrincipalUnitEquivOfPreserves

L215 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.unitsModPrincipalUnitEquivOfPreserves
Documentation

A valuation-ring-preserving field automorphism induces an automorphism on O^*/U^n for every concrete principal-unit level.

Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
open ValuationTheory
open ValuationTheory.DiscreteValuationField.ResidueField
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
Lean source · statement
def unitsModPrincipalUnitEquivOfPreserves
    (e : K ≃+* K)
    (hmem :
      ∀ x : K,
        x ∈ F.valuation.valuationSubring ↔
          e x ∈ F.valuation.valuationSubring)
    (n : ℕ) :
    F.valuationSubringˣ ⧸ higherPrincipalUnitGroup F n ≃*
      F.valuationSubringˣ ⧸ higherPrincipalUnitGroup F n
theorem

unitsModPrincipalUnitEquivOfPreserves_mk

L234 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.unitsModPrincipalUnitEquivOfPreserves_mk
Documentation

Establishes the identity unitsModPrincipalUnitEquivOfPreserves F e hmem n (QuotientGroup.mk' (higherPrincipalUnitGroup F n) u) = QuotientGroup.mk' (higherPrincipalUnitGroup F n) (valuationSubringUnitEquivOfPreserves F e hmem u).

Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
open ValuationTheory
open ValuationTheory.DiscreteValuationField.ResidueField
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
Lean source · statement
theorem unitsModPrincipalUnitEquivOfPreserves_mk
    (e : K ≃+* K)
    (hmem :
      ∀ x : K,
        x ∈ F.valuation.valuationSubring ↔
          e x ∈ F.valuation.valuationSubring)
    (n : ℕ) (u : F.valuationSubringˣ) :
    unitsModPrincipalUnitEquivOfPreserves F e hmem n
        (QuotientGroup.mk' (higherPrincipalUnitGroup F n) u) =
      QuotientGroup.mk' (higherPrincipalUnitGroup F n)
        (valuationSubringUnitEquivOfPreserves F e hmem u)
theorem

unitEquiv_div_mem_principalUnit_one_of_residueUnitHom_fixed

L249 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.unitEquiv_div_mem_principalUnit_one_of_residueUnitHom_fixed
Documentation

If the induced action on residue-field units is trivial, then the valuation-ring unit displacement lies in the first principal-unit group.

Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
open ValuationTheory
open ValuationTheory.DiscreteValuationField.ResidueField
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
Lean source · statement
theorem unitEquiv_div_mem_principalUnit_one_of_residueUnitHom_fixed
    (e : K ≃+* K)
    (hmem :
      ∀ x : K,
        x ∈ F.valuation.valuationSubring ↔
          e x ∈ F.valuation.valuationSubring)
    (hres :
      ∀ u : F.valuationSubringˣ,
        higherPrincipalUnitGroup.residueUnitHom F
            (valuationSubringUnitEquivOfPreserves F e hmem u) =
          higherPrincipalUnitGroup.residueUnitHom F u)
    (u : F.valuationSubringˣ) :
    valuationSubringUnitEquivOfPreserves F e hmem u / u ∈
      higherPrincipalUnitGroup F 1
theorem

unitEquiv_mod_principalUnit_one_eq_of_residueUnitHom_fixed

L270 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.unitEquiv_mod_principalUnit_one_eq_of_residueUnitHom_fixed
Documentation

Quotient form of unitEquiv_div_mem_principalUnit_one_of_residueUnitHom_fixed: residue-trivial unit action fixes O^*/U^1.

Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
open ValuationTheory
open ValuationTheory.DiscreteValuationField.ResidueField
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
Lean source · statement
theorem unitEquiv_mod_principalUnit_one_eq_of_residueUnitHom_fixed
    (e : K ≃+* K)
    (hmem :
      ∀ x : K,
        x ∈ F.valuation.valuationSubring ↔
          e x ∈ F.valuation.valuationSubring)
    (hres :
      ∀ u : F.valuationSubringˣ,
        higherPrincipalUnitGroup.residueUnitHom F
            (valuationSubringUnitEquivOfPreserves F e hmem u) =
          higherPrincipalUnitGroup.residueUnitHom F u)
    (u : F.valuationSubringˣ) :
    QuotientGroup.mk' (higherPrincipalUnitGroup F 1)
        (valuationSubringUnitEquivOfPreserves F e hmem u) =
      QuotientGroup.mk' (higherPrincipalUnitGroup F 1) u
theorem

unitEquiv_div_mem_principalUnit_one_of_residueFieldEquiv_fixed

L297 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.unitEquiv_div_mem_principalUnit_one_of_residueFieldEquiv_fixed
Documentation

Residue-field fixed-point form of unitEquiv_div_mem_principalUnit_one_of_residueUnitHom_fixed: if the induced residue-field automorphism is pointwise trivial, then every valuation-ring unit has first-principal-unit displacement.

Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
open ValuationTheory
open ValuationTheory.DiscreteValuationField.ResidueField
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
Lean source · statement
theorem unitEquiv_div_mem_principalUnit_one_of_residueFieldEquiv_fixed
    (e : K ≃+* K)
    (hmem :
      ∀ x : K,
        x ∈ F.valuation.valuationSubring ↔
          e x ∈ F.valuation.valuationSubring)
    (hres :
      ∀ x : F.residueField,
        valuationSubringResidueFieldEquivOfPreserves F e hmem x = x)
    (u : F.valuationSubringˣ) :
    valuationSubringUnitEquivOfPreserves F e hmem u / u ∈
      higherPrincipalUnitGroup F 1
theorem

unitEquiv_mod_principalUnit_one_eq_of_residueFieldEquiv_fixed

L322 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.unitEquiv_mod_principalUnit_one_eq_of_residueFieldEquiv_fixed
Documentation

Quotient form of unitEquiv_div_mem_principalUnit_one_of_residueFieldEquiv_fixed.

Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
open ValuationTheory
open ValuationTheory.DiscreteValuationField.ResidueField
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
Lean source · statement
theorem unitEquiv_mod_principalUnit_one_eq_of_residueFieldEquiv_fixed
    (e : K ≃+* K)
    (hmem :
      ∀ x : K,
        x ∈ F.valuation.valuationSubring ↔
          e x ∈ F.valuation.valuationSubring)
    (hres :
      ∀ x : F.residueField,
        valuationSubringResidueFieldEquivOfPreserves F e hmem x = x)
    (u : F.valuationSubringˣ) :
    QuotientGroup.mk' (higherPrincipalUnitGroup F 1)
        (valuationSubringUnitEquivOfPreserves F e hmem u) =
      QuotientGroup.mk' (higherPrincipalUnitGroup F 1) u
theorem

unitsModPrincipalUnitEquivOfPreserves_one_apply_eq_of_residueFieldEquiv_fixed

L345 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.unitsModPrincipalUnitEquivOfPreserves_one_apply_eq_of_residueFieldEquiv_fixed
Documentation

If the induced residue-field automorphism is pointwise trivial, then the induced automorphism of O^*/U^1 is pointwise trivial.

Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
open ValuationTheory
open ValuationTheory.DiscreteValuationField.ResidueField
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
Lean source · statement
theorem unitsModPrincipalUnitEquivOfPreserves_one_apply_eq_of_residueFieldEquiv_fixed
    (e : K ≃+* K)
    (hmem :
      ∀ x : K,
        x ∈ F.valuation.valuationSubring ↔
          e x ∈ F.valuation.valuationSubring)
    (hres :
      ∀ x : F.residueField,
        valuationSubringResidueFieldEquivOfPreserves F e hmem x = x)
    (q : F.valuationSubringˣ ⧸ higherPrincipalUnitGroup F 1) :
    unitsModPrincipalUnitEquivOfPreserves F e hmem 1 q = q
theorem

unitsModPrincipalUnitEquivOfPreserves_one_eq_refl_of_residueFieldEquiv_fixed

L364 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.unitsModPrincipalUnitEquivOfPreserves_one_eq_refl_of_residueFieldEquiv_fixed
Documentation

Equivalence form of unitsModPrincipalUnitEquivOfPreserves_one_apply_eq_of_residueFieldEquiv_fixed.

Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
open ValuationTheory
open ValuationTheory.DiscreteValuationField.ResidueField
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
Lean source · statement
theorem unitsModPrincipalUnitEquivOfPreserves_one_eq_refl_of_residueFieldEquiv_fixed
    (e : K ≃+* K)
    (hmem :
      ∀ x : K,
        x ∈ F.valuation.valuationSubring ↔
          e x ∈ F.valuation.valuationSubring)
    (hres :
      ∀ x : F.residueField,
        valuationSubringResidueFieldEquivOfPreserves F e hmem x = x) :
    unitsModPrincipalUnitEquivOfPreserves F e hmem 1 =
      MulEquiv.refl (F.valuationSubringˣ ⧸ higherPrincipalUnitGroup F 1)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.