Vierkantor

# nl_NL
# Translated by Raeon

gui.building.resources=Bouwmaterialen
gui.del=Del
gui.filling.resources=Opvulmaterialen
gui.inventory=Inventaris
gui.lock=Sluiten
gui.needed=Nodig
gui.unlock=Openen

Vierkantor

import tactic

universes u

variables {α : Type u}

/-- `invertible a` gives a two-sided multiplicative inverse of `a` -/
class invertible [has_mul α] [has_one α] (a : α) : Type u :=
(inv_of : α) (inv_of_mul_self : inv_of * a = 1) (mul_inv_of_self : a * inv_of = 1)

Vierkantor

import Mathlib

open Lean Elab Command

/-- Get the top-level directory for this name.

For example: (`Mathlib.Data.Nat.Init).topLevel = `Mathlib.Data.
-/
partial def Lean.Name.topLevel (n : Name) (length := 2) : Name :=
  if n.getNumParts <= length then n else n.getPrefix.topLevel (length := length)

Vierkantor

✔ [0/859] Ran mathlib:extraDep
✔ [1/859] Replayed Mathlib.Tactic.Linter.DirectoryDependency
✔ [2/859] Replayed Mathlib.Tactic.Linter.Header
✔ [3/859] Replayed Mathlib.Tactic.Linter.CommandStart
✔ [4/859] Replayed Mathlib.Tactic.Linter.DeprecatedSyntaxLinter
✔ [5/859] Replayed Mathlib.Tactic.Linter.DocPrime
✔ [6/859] Replayed Mathlib.Tactic.Linter.DocString
✔ [7/859] Replayed Mathlib.Tactic.Linter.GlobalAttributeIn
✔ [8/859] Replayed Mathlib.Tactic.Linter.HashCommandLinter
✔ [9/859] Replayed Mathlib.Tactic.Linter.FlexibleLinter