FLT/Mathlib/Topology/Algebra/Valued/ValuationTopology.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Valuation Topology

Material destined for Mathlib.

Imports (1)
Imported by 2 files
  1. lemma Valued.isUnit_valuationSubring_iff line 21 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Field, LinearOrderedCommGroupWithZero, Valued, Subtype, Membership.mem, ValuationSubring, Valuation.valuationSubring, Valued.v, Iff, IsUnit, Eq, Valuation, OfNat.ofNat

    Proof uses: Eq.mpr, RingHom, Algebra.algebraMap, eq_of_heq, HEq, Eq.refl, HEq.refl, Eq.symm, outParam, DFunLike, heq_of_eq, Valuation.Integers.isUnit_iff_valuation_eq_one, Valuation.integer.integers

    61 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

    Open to load the checked before-and-after goal states.