From 48e0e568db0a58a8a1bf402fd7de8af21e9c7227 Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Tue, 12 May 2026 12:42:52 +0200 Subject: [PATCH] chore: add more codeblocks --- Mathlib/Algebra/Lie/Classical.lean | 46 +++++++++++-------- Mathlib/Data/List/Defs.lean | 6 ++- Mathlib/Data/Num/Basic.lean | 14 ++++-- Mathlib/Data/Num/Bitwise.lean | 25 ++++++---- .../RingedSpace/PresheafedSpace/Gluing.lean | 4 ++ 5 files changed, 61 insertions(+), 34 deletions(-) diff --git a/Mathlib/Algebra/Lie/Classical.lean b/Mathlib/Algebra/Lie/Classical.lean index 032b7a8fcd3886..17bc1eeee7990d 100644 --- a/Mathlib/Algebra/Lie/Classical.lean +++ b/Mathlib/Algebra/Lie/Classical.lean @@ -238,8 +238,10 @@ theorem soIndefiniteEquiv_apply {i : R} (hi : i * i = -1) (A : so' p q R) : It looks like this as a `2l x 2l` matrix of `l x l` blocks: - [ 0 1 ] - [ 1 0 ] +``` +[ 0 1 ] +[ 1 0 ] +``` -/ def JD : Matrix (l ⊕ l) (l ⊕ l) R := Matrix.fromBlocks 0 1 1 0 @@ -254,9 +256,10 @@ diagonal matrix. It looks like this as a `2l x 2l` matrix of `l x l` blocks: - [ 1 -1 ] - [ 1 1 ] --/ +``` +[ 1 -1 ] +[ 1 1 ] +``` -/ def PD : Matrix (l ⊕ l) (l ⊕ l) R := Matrix.fromBlocks 1 (-1) 1 1 @@ -295,15 +298,19 @@ noncomputable def typeDEquivSo' [Fintype l] [Invertible (2 : R)] : typeD l R ≃ It looks like this as a `(2l+1) x (2l+1)` matrix of blocks: - [ 2 0 0 ] - [ 0 0 1 ] - [ 0 1 0 ] +``` +[ 2 0 0 ] +[ 0 0 1 ] +[ 0 1 0 ] +``` where sizes of the blocks are: - [`1 x 1` `1 x l` `1 x l`] - [`l x 1` `l x l` `l x l`] - [`l x 1` `l x l` `l x l`] +``` +[`1 x 1` `1 x l` `1 x l`] +[`l x 1` `l x l` `l x l`] +[`l x 1` `l x l` `l x l`] +``` -/ def JB := Matrix.fromBlocks ((2 : R) • (1 : Matrix Unit Unit R)) 0 0 (JD l R) @@ -318,16 +325,19 @@ almost-split-signature diagonal matrix. It looks like this as a `(2l+1) x (2l+1)` matrix of blocks: - [ 1 0 0 ] - [ 0 1 -1 ] - [ 0 1 1 ] +``` +[ 1 0 0 ] +[ 0 1 -1 ] +[ 0 1 1 ] +``` where sizes of the blocks are: - [`1 x 1` `1 x l` `1 x l`] - [`l x 1` `l x l` `l x l`] - [`l x 1` `l x l` `l x l`] --/ +``` +[`1 x 1` `1 x l` `1 x l`] +[`l x 1` `l x l` `l x l`] +[`l x 1` `l x l` `l x l`] +``` -/ def PB := Matrix.fromBlocks (1 : Matrix Unit Unit R) 0 0 (PD l R) diff --git a/Mathlib/Data/List/Defs.lean b/Mathlib/Data/List/Defs.lean index f445ce3226a31a..2898b717c99af0 100644 --- a/Mathlib/Data/List/Defs.lean +++ b/Mathlib/Data/List/Defs.lean @@ -240,9 +240,11 @@ instance instSProd : SProd (List α) (List β) (List (α × β)) where sprod := List.product /-- `dedup l` removes duplicates from `l` (taking only the last occurrence). - Defined as `pwFilter (≠)`. +Defined as `pwFilter (≠)`. - dedup [1, 0, 2, 2, 1] = [0, 2, 1] -/ +``` +dedup [1, 0, 2, 2, 1] = [0, 2, 1] +``` -/ def dedup [DecidableEq α] : List α → List α := pwFilter (· ≠ ·) diff --git a/Mathlib/Data/Num/Basic.lean b/Mathlib/Data/Num/Basic.lean index b351f160f5278f..e3ba2128f69f56 100644 --- a/Mathlib/Data/Num/Basic.lean +++ b/Mathlib/Data/Num/Basic.lean @@ -23,7 +23,9 @@ collection of theorems is to show the equivalence of the different approaches. /-- The type of positive binary numbers. - 13 = 1101(base 2) = bit1 (bit0 (bit1 one)) -/ +``` +13 = 1101(base 2) = bit1 (bit0 (bit1 one)) +``` -/ inductive PosNum : Type | one : PosNum | bit1 : PosNum → PosNum @@ -38,7 +40,9 @@ instance : Inhabited PosNum := /-- The type of nonnegative binary numbers, using `PosNum`. - 13 = 1101(base 2) = pos (bit1 (bit0 (bit1 one))) -/ +``` +13 = 1101(base 2) = pos (bit1 (bit0 (bit1 one))) +``` -/ inductive Num : Type | zero : Num | pos : PosNum → Num @@ -55,8 +59,10 @@ instance : Inhabited Num := /-- Representation of integers using trichotomy around zero. - 13 = 1101(base 2) = pos (bit1 (bit0 (bit1 one))) - -13 = -1101(base 2) = neg (bit1 (bit0 (bit1 one))) -/ +``` +13 = 1101(base 2) = pos (bit1 (bit0 (bit1 one))) +-13 = -1101(base 2) = neg (bit1 (bit0 (bit1 one))) +``` -/ inductive ZNum : Type | zero : ZNum | pos : PosNum → ZNum diff --git a/Mathlib/Data/Num/Bitwise.lean b/Mathlib/Data/Num/Bitwise.lean index 19e45a4875b1df..5abcd4081498d4 100644 --- a/Mathlib/Data/Num/Bitwise.lean +++ b/Mathlib/Data/Num/Bitwise.lean @@ -216,20 +216,25 @@ inductive NzsNum : Type | bit : Bool → NzsNum → NzsNum deriving DecidableEq -/-- Alternative representation of integers using a sign bit at the end. - The convention on sign here is to have the argument to `msb` denote - the sign of the MSB itself, with all higher bits set to the negation - of this sign. The result is interpreted in two's complement. +/-- +Alternative representation of integers using a sign bit at the end. +The convention on sign here is to have the argument to `msb` denote +the sign of the MSB itself, with all higher bits set to the negation +of this sign. The result is interpreted in two's complement. - 13 = ..0001101(base 2) = nz (bit1 (bit0 (bit1 (msb true)))) - -13 = ..1110011(base 2) = nz (bit1 (bit1 (bit0 (msb false)))) +``` +13 = ..0001101(base 2) = nz (bit1 (bit0 (bit1 (msb true)))) +-13 = ..1110011(base 2) = nz (bit1 (bit1 (bit0 (msb false)))) +``` As with `Num`, a special case must be added for zero, which has no msb, - but by two's complement symmetry there is a second special case for -1. - Here the `Bool` field indicates the sign of the number. +but by two's complement symmetry there is a second special case for -1. +Here the `Bool` field indicates the sign of the number. - 0 = ..0000000(base 2) = zero false - -1 = ..1111111(base 2) = zero true -/ +``` +0 = ..0000000(base 2) = zero false +-1 = ..1111111(base 2) = zero true +``` -/ inductive SNum : Type | zero : Bool → SNum | nz : NzsNum → SNum diff --git a/Mathlib/Geometry/RingedSpace/PresheafedSpace/Gluing.lean b/Mathlib/Geometry/RingedSpace/PresheafedSpace/Gluing.lean index 178cfb54c14eab..9ab7b6f40b6d4f 100644 --- a/Mathlib/Geometry/RingedSpace/PresheafedSpace/Gluing.lean +++ b/Mathlib/Geometry/RingedSpace/PresheafedSpace/Gluing.lean @@ -489,10 +489,12 @@ instance ιIsOpenImmersion (i : D.J) : IsOpenImmersion (𝖣.ι i) where set_option backward.isDefEq.respectTransparency false in /-- The following diagram is a pullback, i.e. `Vᵢⱼ` is the intersection of `Uᵢ` and `Uⱼ` in `X`. +``` Vᵢⱼ ⟶ Uᵢ | | ↓ ↓ Uⱼ ⟶ X +``` -/ def vPullbackConeIsLimit (i j : D.J) : IsLimit (𝖣.vPullbackCone i j) := PullbackCone.isLimitAux' _ fun s => by @@ -589,10 +591,12 @@ theorem ι_jointly_surjective (x : 𝖣.glued) : ∃ (i : D.J) (y : D.U i), ( /-- The following diagram is a pullback, i.e. `Vᵢⱼ` is the intersection of `Uᵢ` and `Uⱼ` in `X`. +``` Vᵢⱼ ⟶ Uᵢ | | ↓ ↓ Uⱼ ⟶ X +``` -/ def vPullbackConeIsLimit (i j : D.J) : IsLimit (𝖣.vPullbackCone i j) := 𝖣.vPullbackConeIsLimitOfMap forgetToPresheafedSpace i j