PFR/Mathlib/LinearAlgebra/Quotient/Basic.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Imports (1)
Imported by 2 files
  1. instance Submodule.Quotient.finite line 7 source

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

    Statement uses: Ring, AddCommGroup, Module, Finite, Submodule, HasQuotient.Quotient

    Proof uses: Fintype, Nonempty, Eq, nonempty_fintype, Nonempty.intro, inferInstance, Eq.refl

    9 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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