Skip to content

Commit

Permalink
fix: fix link in docstring of IsWellFounded (#7063)
Browse files Browse the repository at this point in the history
  • Loading branch information
ADedecker committed Sep 10, 2023
1 parent 4a23855 commit f39f702
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion Mathlib/Order/RelClasses.lean
Expand Up @@ -271,7 +271,7 @@ instance (priority := 100) isStrictTotalOrder_of_isStrictTotalOrder [IsStrictTot
/-! ### Well-order -/


/-- A well-founded relation. Not to be confused with `isWellOrder`. -/
/-- A well-founded relation. Not to be confused with `IsWellOrder`. -/
@[mk_iff] class IsWellFounded (α : Type u) (r : α → α → Prop) : Prop where
/-- The relation is `WellFounded`, as a proposition. -/
wf : WellFounded r
Expand Down

0 comments on commit f39f702

Please sign in to comment.