PFR/Mathlib/LinearAlgebra/Dimension/FreeAndStrongRankCondition.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Imports (1)
Imported by 2 files
  1. theorem cardinal_le_aleph0_of_finiteDimensional line 15 source

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

    Statement uses: Ring, StrongRankCondition, AddCommGroup, Module, Module.Free, Module.Finite, Countable, LE.le, Cardinal, Cardinal.mk, Cardinal.aleph0

    Proof uses: Eq.mpr, Cardinal.lift, id, Eq, congrArg, Eq.symm, propext, Cardinal.lift_le_aleph0, HPow.hPow, Module.rank, lift_cardinalMk_eq_lift_cardinalMk_field_pow_lift_rank, Cardinal.power_le_aleph0, Iff.mpr, Cardinal.mk_le_aleph0_iff, LT.lt, Cardinal.lift_lt_aleph0, Module.rank_lt_aleph0

    11 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  2. theorem countable_of_finiteDimensional line 22 source

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

    Statement uses: Ring, StrongRankCondition, AddCommGroup, Module, Module.Free, Module.Finite, Countable

    Proof uses: LE.le, Cardinal, Cardinal.mk, Cardinal.aleph0, cardinal_le_aleph0_of_finiteDimensional, Iff.mp, Cardinal.mk_le_aleph0_iff

    5 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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