mathlib
4a8fb6a3 - chore(linear_algebra): rename endomorphism multiplicative structures for consistency (#9336)

Commit
4 years ago
chore(linear_algebra): rename endomorphism multiplicative structures for consistency (#9336) This renames: * `module.endomorphism_semiring` → `module.End.semiring` * `module.endomorphism_ring` → `module.End.ring` * `module.endomorphism_algebra` → `module.End.algebra` * `linear_map.module.End.division_ring` → `module.End.division_ring` This brings the name in line with the names for `add_monoid.End`. Since `module.End` is an abbreviation, it does not matter that the instances now use this instead of `M →ₗ[R] M`.
Author
Parents
Loading