kronecker): make the `R` argument implicit (#18624)

Commit

2 years ago

chore(data/matrix/kronecker): make the `R` argument implicit (#18624) This was copied erroneously from the `tensor_product` section, where an explicit `R` _is_ needed.

Author

eric-wieser

Parents

540b766a

mathlib 945bc74e - chore(data/matrix/kronecker): make the `R` argument implicit (#18624)

mathlib
945bc74e - chore(data/matrix/kronecker): make the `R` argument implicit (#18624)