Code Snippets Lean

Short texts Lean πŸ§‘β€πŸ’» Code snippets Lean ✍️ Reading lists Lean πŸ‘€

sim_option_rec.lean

/- Define a “nonzero” type -/ import algebra.group universe u variables {M : Type*} structure nonzero (Ξ± : Type u) [C : has_zero Ξ±] := (val : Ξ±) (not_zero : val β‰  0) namespace nonzero variable [has_zero M] instance : has_coe (nonzero M) M := ⟨val⟩ @[ext] theorem ext : function.injective (coe : nonzero M […]

BalkanMOP2.lean

import data.real.basic import algebra import tactic import algebra.quadratic_discriminant import algebra.ordered_field import algebra.ordered_group import algebra.ordered_ring open classical local attribute [instance] prop_decidable theorem geq_one (a b : ℝ) (ha: 1 ≀ a) (hb: 1 ≀ b): 1 ≀ a * b := begin have ha’: 0 ≀ a, {linarith,}, calc 1 ≀ a: by exact ha … […]

lie-semisimple-classification.lean

import algebra.lie.classical import algebra.lie.cartan_matrix import algebra.lie.semisimple import algebra.lie.direct_sum import field_theory.algebraic_closure open fintype lie_algebra open_locale direct_sum notation L₁ ` ≅ₗ⁅` K `⁆ `Lβ‚‚ := nonempty (L₁ ≃ₗ⁅K⁆ Lβ‚‚) abbreviation sl (l : β„•) (K : Type*) [field K] := lie_algebra.special_linear.sl (fin l) K abbreviation sp (l : β„•) (K : Type*) [field K] := lie_algebra.symplectic.sp (fin […]

knight_knave_sol.lean

import tactic /- # Knight and Knaves. In a remote village there lives knights and knaves. The knights are honourable and thus, speaks only the truth. On the other hand, the knaves are mischievious and thus, lies out of their teeth. One day, you decided to visit this village and villagers `A`, `B` and `C` […]