Skip to content

Commit 3c5419f

Browse files
committed
doc: recommended_spelling for +ᵥ and -ᵥ (leanprover-community#34672)
Co-authored-by: Komyyy <pol_tta@outlook.jp>
1 parent f8ec307 commit 3c5419f

1 file changed

Lines changed: 3 additions & 0 deletions

File tree

Mathlib/Algebra/Notation/Defs.lean

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -70,6 +70,9 @@ attribute [ext] SMul VAdd
7070
@[inherit_doc] infixr:65 " +ᵥ " => HVAdd.hVAdd
7171
@[inherit_doc] infixl:65 " -ᵥ " => VSub.vsub
7272

73+
recommended_spelling "vadd" for "+ᵥ" in [HVAdd.hVAdd, «term_+ᵥ_»]
74+
recommended_spelling "vsub" for "-ᵥ" in [VSub.vsub, «term_-ᵥ_»]
75+
7376
attribute [to_additive existing] Mul Div HMul instHMul HDiv instHDiv HSMul
7477
attribute [to_additive (reorder := 1 2) SMul] Pow
7578
attribute [to_additive (reorder := 1 2)] HPow

0 commit comments

Comments
 (0)