FLT/Mathlib/LinearAlgebra/Determinant.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma mulLeft_conj line 33 source

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

   Statement uses: Field, Ring, Algebra, Nat, TensorProduct, AlgEquiv, Matrix, Fin, Eq, LinearMap, RingHom.id, LinearMap.mulLeft, LinearMap.comp, AlgEquiv.symm

   Proof uses: LinearMap.ext, of_eq_true, HMul.hMul, Eq.trans, True, forall_congr, congrArg, map_mul, MonoidHom.id, AlgEquiv.apply_symm_apply, eq_self, implies_true

   86 instances, coercions and auxiliary constants left out.

   Tactic trace: 2 steps

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

2. lemma mulRight_conj line 39 source

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

   Statement uses: Field, Ring, Algebra, Nat, TensorProduct, AlgEquiv, Matrix, Fin, Eq, LinearMap, RingHom.id, LinearMap.mulRight, LinearMap.comp, AlgEquiv.symm

   Proof uses: LinearMap.ext, of_eq_true, HMul.hMul, Eq.trans, True, forall_congr, congrArg, map_mul, MonoidHom.id, congrFun', AlgEquiv.apply_symm_apply, eq_self, implies_true

   86 instances, coercions and auxiliary constants left out.

   Tactic trace: 2 steps

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

3. lemma mulLeft_conj_ofLinear line 45 source

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

   Statement uses: Field, Nat, Matrix, Fin, Eq, LinearMap, RingHom.id, LinearMap.comp, LinearEquiv.symm, LinearEquiv.trans, Matrix.ofLinearEquiv, Matrix.transposeLinearEquiv, LinearMap.mulLeft, LinearMap.pi, LinearEquiv, Matrix.toLin', LinearMap.proj

   Proof uses: rfl

   66 instances, coercions and auxiliary constants left out.

4. lemma mulRight_conj_ofLinear line 51 source

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

   Statement uses: Field, Nat, Matrix, Fin, Eq, LinearMap, RingHom.id, LinearMap.comp, LinearEquiv.symm, Matrix.ofLinearEquiv, LinearMap.mulRight, LinearMap.pi, LinearEquiv, Matrix.toLin', Matrix.transpose, LinearMap.proj

   Proof uses: LinearMap.ext, funext, of_eq_true, Finset.sum, Finset.univ, HMul.hMul, Eq.trans, True, congrFun', congrArg, Equiv, Matrix.of, mul_comm, eq_self

   91 instances, coercions and auxiliary constants left out.

   Tactic trace: 4 steps

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

5. instance (instance at line 68) line 68 source

   Source documentation

   This is instance is in a repo on brauergroup which has been PRed into mathlib at https://github.com/leanprover-community/mathlib4/pull/26377 . The associated FLT issue is #631. For now it's in import FLT.Mathlib.RingTheory.SimpleRing.TensorProduct.

   instance (A B : Type*) [Ring A] [Ring B] [Algebra k A] [Algebra k B]
       [Algebra.IsCentral k B] [IsSimpleRing A] [IsSimpleRing B] : IsSimpleRing (B ⊗[k] A) :=
   …

6. instance (instance at line 72) line 72 source
7. lemma IsSimpleRing.mulLeft_det_eq_mulRight_det line 77 source

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

   Statement uses: Field, Ring, Algebra, Algebra.IsCentral, IsSimpleRing, FiniteDimensional, Eq, MonoidHom, LinearMap, RingHom.id, LinearMap.det, LinearMap.mulLeft, LinearMap.mulRight

   Proof uses: AlgebraicClosure, Nat, Exists, NeZero, Nonempty, AlgEquiv, TensorProduct, Matrix, Fin, IsSimpleRing.exists_algEquiv_matrix_of_isAlgClosed, LinearMap.baseChange, TensorProduct.tmul, OfNat.ofNat, TensorProduct.AlgebraTensorModule.curry_injective, LinearMap.ext_ring, TensorProduct.AlgebraTensorModule.curry, LinearMap.ext, of_eq_true, Eq.trans, HMul.hMul and 46 more

   153 instances, coercions and auxiliary constants left out.

   Tactic trace: 18 steps

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

8. lemma IsSimpleRing.mulLeft_det_eq_mulRight_det' line 103 source

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

   Statement uses: Field, Ring, Algebra, Algebra.IsCentral, IsSimpleRing, FiniteDimensional, Units, Eq, MonoidHom, LinearEquiv, RingHom.id, LinearEquiv.det, LinearEquiv.mulLeft, LinearEquiv.mulRight

   Proof uses: Units.ext, of_eq_true, LinearMap, LinearMap.det, LinearMap.mulRight, Eq.trans, True, congrFun', congrArg, IsSimpleRing.mulLeft_det_eq_mulRight_det, eq_self

   52 instances, coercions and auxiliary constants left out.

   Tactic trace: 2 steps

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

9. lemma LinearEquiv.det_ne_zero line 118 source

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

   Statement uses: CommRing, Nontrivial, AddCommGroup, Module, LinearEquiv, RingHom.id, Ne, MonoidHom, LinearMap, LinearMap.det, OfNat.ofNat

   Proof uses: IsUnit.ne_zero, LinearEquiv.isUnit_det'

   28 instances, coercions and auxiliary constants left out.

10. lemma Matrix.toLinearEquiv_toLinearMap line 122 source

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

    Statement uses: CommRing, Fintype, DecidableEq, AddCommGroup, Module, Module.Basis, Matrix, IsUnit, Matrix.det, Eq, LinearMap, RingHom.id, Matrix.toLinearEquiv, LinearEquiv, Matrix.toLin

    Proof uses: rfl

    30 instances, coercions and auxiliary constants left out.

11. lemma LinearEquiv.det_toLinearEquiv line 126 source

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

    Statement uses: CommRing, Fintype, DecidableEq, AddCommGroup, Module, Module.Basis, Matrix, IsUnit, Matrix.det, Eq, Units, MonoidHom, LinearEquiv, RingHom.id, LinearEquiv.det, Matrix.toLinearEquiv, IsUnit.unit

    Proof uses: Iff.mp, Units.val_inj, of_eq_true, Eq.trans, True, congrFun', congrArg, LinearMap.det_toLin, eq_self

    29 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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