FLT/Mathlib/LinearAlgebra/TensorProduct/Basis.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Basis

Material destined for Mathlib.

Imports (3)
Imported by 2 files
  1. instance (instance at line 24) line 24 source

    Source documentation

    If A is a nontrivial free R-module and B is a nontrivial R-module then A ⊗[R] B is also nontrivial.

    instance (R : Type*) [CommSemiring R] (A B : Type*) [AddCommMonoid A] [AddCommMonoid B]
    [Module R A] [Module R B] [Module.Free R A] [Nontrivial A] [Nontrivial B] :
    Nontrivial (A ⊗[R] B) := by
…
  2. instance (instance at line 35) line 35 source

    Source documentation

    If A is a nontrivial R-module and B is a nontrivial free R-module then A ⊗[R] B is also nontrivial.

    instance (R : Type*) [CommSemiring R] (A B : Type*) [AddCommMonoid A] [AddCommMonoid B]
    [Module R A] [Module R B] [Module.Free R B] [Nontrivial A] [Nontrivial B] :
    Nontrivial (A ⊗[R] B) := by
…