Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-27 12:53 ba9c8f35

View on Github →

feat(ring_theory/tensor_product): A predicate for being the tensor product. (#15512)

Estimated changes

Created src/ring_theory/is_tensor_product.lean

added def is_base_change.equiv

added theorem is_base_change.equiv_symm_apply

added theorem is_base_change.equiv_tmul

added def is_base_change.lift

added theorem is_base_change.lift_comp

added theorem is_base_change.lift_eq

added def is_base_change

added def is_tensor_product.equiv

added theorem is_tensor_product.equiv_symm_apply

added theorem is_tensor_product.equiv_to_linear_map

added theorem is_tensor_product.induction_on

added def is_tensor_product.lift

added theorem is_tensor_product.lift_eq

added def is_tensor_product.map

added theorem is_tensor_product.map_eq

added def is_tensor_product

added theorem tensor_product.is_base_change

added theorem tensor_product.is_tensor_product