Skip to content

Commit

Permalink
chore(data/finsupp/fin): fix spacing (#14860)
Browse files Browse the repository at this point in the history
  • Loading branch information
vihdzp committed Jun 21, 2022
1 parent 326465d commit 8ac19d3
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/data/finsupp/fin.lean
Expand Up @@ -5,6 +5,7 @@ Authors: Ivan Sadofschi Costa
-/
import data.fin.tuple
import data.finsupp.basic

/-!
# `cons` and `tail` for maps `fin n →₀ M`
Expand All @@ -24,7 +25,6 @@ namespace finsupp
variables {n : ℕ} (i : fin n) {M : Type*} [has_zero M] (y : M)
(t : fin (n + 1) →₀ M) (s : fin n →₀ M)


/-- `tail` for maps `fin (n + 1) →₀ M`. See `fin.tail` for more details. -/
def tail (s : fin (n + 1) →₀ M) : fin n →₀ M :=
finsupp.equiv_fun_on_fintype.inv_fun (fin.tail s.to_fun)
Expand Down

0 comments on commit 8ac19d3

Please sign in to comment.