Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-14 09:01 58dde5b8

View on Github →

chore(*): generalize tensor product to semirings (#3389)

Estimated changes

Modified src/data/polynomial.lean

Modified src/linear_algebra/tensor_product.lean

added inductive tensor_product.eqv

deleted theorem tensor_product.lift_aux.add

modified theorem tensor_product.lift_aux.smul

modified def tensor_product.lift_aux

added theorem tensor_product.lift_aux_tmul

deleted def tensor_product.relators

modified def tensor_product.smul.aux

added theorem tensor_product.smul.aux_of

added theorem tensor_product.smul_tmul'

modified def tensor_product.tmul

modified theorem tensor_product.tmul_zero

modified theorem tensor_product.zero_tmul

Modified src/ring_theory/matrix_algebra.lean

Modified src/ring_theory/polynomial_algebra.lean

Modified src/ring_theory/tensor_product.lean