Skip to content

Commit 69cbc3c

Browse files
committed
chore: avoid 'adaptation note' substring in adaptation note bodies
1 parent 5f939f8 commit 69cbc3c

2 files changed

Lines changed: 2 additions & 2 deletions

File tree

Mathlib/LinearAlgebra/Determinant.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -148,7 +148,7 @@ theorem detAux_def' (b : Basis ι A M) (f : M →ₗ[A] M) :
148148
#adaptation_note /-- Proof repaired after leanprover/lean4#13492.
149149
The first line below was previously just `rw [detAux]`.
150150
The replacement proof is a short-term fix, and we request that the authors/maintainers of
151-
this file review the proof, and either approve it by removing this adaptation note, revise
151+
this file review the proof, and either approve it by removing this note, revise
152152
the proof or the prerequisites appropriately, or minimize a problem in lean4 that still
153153
needs addressing. -/
154154
simp only [detAux_def, Trunc.lift_mk]

Mathlib/Order/JordanHolder.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -297,7 +297,7 @@ The proof body used to be a single term
297297
(where `e` was defined via the same `calc` block; the signature had `: ... :=` rather
298298
than `: ... := by`).
299299
The replacement proof is a short-term fix, and we request that the authors/maintainers of
300-
this file review the proof, and either approve it by removing this adaptation note, revise
300+
this file review the proof, and either approve it by removing this note, revise
301301
the proof or the prerequisites appropriately, or minimize a problem in lean4 that still
302302
needs addressing. -/
303303
set_option backward.isDefEq.respectTransparency false in

0 commit comments

Comments
 (0)