Mathlib v3 is deprecated. Go to Mathlib v4

Def finsupp.lcomap_domain

Modification history

2022-11-30 10:44
src/linear_algebra/finsupp.lean
feat(ring_theory): `is_adjoin_root` predicate (#17690) …
Added finsupp.lcomap_domainView on Github →