Skip to content

Commit 3b2e97b

Browse files
committed
chore(Algebra/Homology): fix ComplexShape.boundaryLE_embeddingUpIntLE_iff (leanprover-community#25673)
This PR fixes the statement of the lemma `boundaryLE_embeddingUpIntLE_iff`.
1 parent eb9a848 commit 3b2e97b

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

Mathlib/Algebra/Homology/Embedding/Boundary.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -184,7 +184,7 @@ lemma boundaryGE_embeddingUpIntGE_iff (p : ℤ) (n : ℕ) :
184184
omega
185185

186186
lemma boundaryLE_embeddingUpIntLE_iff (p : ℤ) (n : ℕ) :
187-
(embeddingUpIntGE p).BoundaryGE n ↔ n = 0 := by
187+
(embeddingUpIntLE p).BoundaryLE n ↔ n = 0 := by
188188
constructor
189189
· intro h
190190
obtain _|n := n

0 commit comments

Comments
 (0)