FLT/Mathlib/RingTheory/Valuation/ValuationSubring.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Valuation Subring

Material destined for Mathlib.

Imports (1)
Imported by 2 files
  1. lemma ValuationSubring.subtype_inj line 20 source

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

    Statement uses: Field, ValuationSubring, Subtype, Membership.mem, Iff, Eq, RingHom, ValuationSubring.subtype

    Proof uses: Function.Injective.eq_iff, ValuationSubring.subtype_injective

    28 instances, coercions and auxiliary constants left out.

  2. theorem ValuationSubring.valued_eq_one_of_isUnit line 24 source

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

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

    Proof uses: Units, le_antisymm, Iff.mp, LE.le, Valuation.mem_valuationSubring_iff, Subtype.property, Eq.mpr, id, congrArg, Eq.symm, Valuation.map_one, Submonoid, Subsemiring.toSubmonoid, Subring.toSubsemiring, ValuationSubring.toSubring, Submonoid.coe_one, HMul.hMul, Inv.inv, Units.mul_inv, Submonoid.coe_mul and 3 more

    92 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

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

  3. theorem ValuationSubring.isUnit_of_valued_eq_one line 34 source

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

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

    Proof uses: Eq.mpr, Ne, id, congrArg, propext, isUnit_iff_ne_zero, Not, ne_eq, Eq.symm, map_eq_zero, of_eq_true, Eq.trans, False, True, not_false_eq_true, Units, LE.le, Inv.inv, HMul.hMul, one_mul and 18 more

    104 instances, coercions and auxiliary constants left out.

    Tactic trace: 10 steps

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

  4. theorem ValuationSubring.isUnit_iff_valued_eq_one line 44 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: Iff.intro, ValuationSubring.valued_eq_one_of_isUnit, ValuationSubring.isUnit_of_valued_eq_one

    54 instances, coercions and auxiliary constants left out.