Mathlib v3 is deprecated. Go to Mathlib v4

Theorem tensor_power.algebra_map₀_one

Modification history

2023-03-30 12:15

src/linear_algebra/tensor_power.lean

feat(linear_algebra/tensor_power): the tensor powers form a graded algebra (#10255)

Added tensor_power.algebra_map₀_one View on Github →