mathlib documentation

core / init.default

source

Imports

init.cc_lemmas
init.classical
init.coe
init.control.combinators
init.core
init.function
init.funext
init.logic
init.meta.float
init.meta.well_founded_tactics
init.propext
init.util
init.version
init.wf

Imported by

data.buffer
data.buffer.parser
data.dlist
system.io
system.io_interface
system.random
2019.questions.sheet1
2019.questions.sheet2
2019.questions.sheet3
2019.questions.sheet4
2019.solutions.sheet3
2020.functions.bijection_game
2020.functions.happy_animals
2020.functions.two_sided_inverse
2020.functions.univ_product
2020.integers.int_def_solns
2020.logic.SAT_example
2020.logic.bool_not
2020.logic.logic_lecture_ad_lib
2020.logic.logic_video
2020.logic.questions
2020.logic.solutions
2020.peano.peano_practice_questions
2020.problem_sheets.Part_II.sheet1_q3
2020.problem_sheets.Part_II_sheet1
2020.relations.equiv_partition2
2020.relations.partition_challenge
2020.relations.partition_challenge_official_solution
2020.relations.partition_challenge_solution2
2020.relations.partition_challenge_xena
2020.relations.random_reln_transitive2
2020.sets.canonical
2020.sets.real_numbers
2020.tactic_hints.examples
2021.functions.sheet1
2021.logic.sheet1
2021.logic.sheet2
2021.logic.sheet3
2021.logic.sheet4
2021.logic.sheet5
2021.logic.sheet6
2021.sets.sheet1
2021.sets.sheet2
2021.sets.sheet3
2021.sets.sheet4
2021.sets.sheet5
2021.sets.sheet6
2021.sets.sheet7
algebra.abs
algebra.algebra.basic
algebra.associated
algebra.big_operators.basic
algebra.big_operators.option
algebra.big_operators.order
algebra.big_operators.pi
algebra.big_operators.ring
algebra.bounds
algebra.char_zero
algebra.covariant_and_contravariant
algebra.divisibility
algebra.euclidean_domain
algebra.field.basic
algebra.field.opposite
algebra.field_power
algebra.free_monoid
algebra.gcd_monoid.basic
algebra.group.basic
algebra.group.commute
algebra.group.conj
algebra.group.defs
algebra.group.hom
algebra.group.hom_instances
algebra.group.inj_surj
algebra.group.opposite
algebra.group.pi
algebra.group.prod
algebra.group.semiconj
algebra.group.to_additive
algebra.group.type_tags
algebra.group.units
algebra.group.units_hom
algebra.group.with_one
algebra.group_action_hom
algebra.group_power.basic
algebra.group_power.lemmas
algebra.group_power.order
algebra.group_ring_action
algebra.group_with_zero.basic
algebra.group_with_zero.defs
algebra.group_with_zero.power
algebra.indicator_function
algebra.invertible
algebra.module.basic
algebra.module.hom
algebra.module.linear_map
algebra.module.pi
algebra.module.prod
algebra.module.submodule
algebra.module.submodule_lattice
algebra.opposites
algebra.order.absolute_value
algebra.order.archimedean
algebra.order.field
algebra.order.floor
algebra.order.group
algebra.order.monoid
algebra.order.monoid_lemmas
algebra.order.nonneg
algebra.order.ring
algebra.order.sub
algebra.order.with_zero
algebra.pointwise
algebra.punit_instances
algebra.quotient
algebra.regular.basic
algebra.regular.smul
algebra.ring.basic
algebra.ring.comp_typeclasses
algebra.ring.opposite
algebra.ring.pi
algebra.ring.prod
algebra.smul_with_zero
algebra.star.basic
algebra.support
category_theory.category.basic
combinatorics.quiver
control.applicative
control.basic
control.bifunctor
control.equiv_functor
control.equiv_functor.instances
control.functor
control.monad.basic
control.traversable.basic
control.traversable.derive
control.traversable.equiv
control.traversable.lemmas
data.array.lemmas
data.bool.all_any
data.bool.basic
data.bool.set
data.char
data.dfinsupp
data.dlist.basic
data.equiv.basic
data.equiv.denumerable
data.equiv.encodable.basic
data.equiv.functor
data.equiv.module
data.equiv.mul_add
data.equiv.mul_add_aut
data.equiv.nat
data.equiv.ring
data.equiv.ring_aut
data.equiv.set
data.fin.basic
data.fin.interval
data.finset.basic
data.finset.card
data.finset.fin
data.finset.fold
data.finset.lattice
data.finset.locally_finite
data.finset.option
data.finset.order
data.finset.pi
data.finset.powerset
data.finset.preimage
data.finset.prod
data.finset.sigma
data.finset.sort
data.finsupp.basic
data.fintype.basic
data.fintype.card
data.fun_like
data.int.basic
data.int.cast
data.int.char_zero
data.int.interval
data.int.least_greatest
data.list.basic
data.list.big_operators
data.list.chain
data.list.count
data.list.defs
data.list.duplicate
data.list.erase_dup
data.list.forall2
data.list.func
data.list.join
data.list.lattice
data.list.lex
data.list.min_max
data.list.nodup
data.list.nodup_equiv_fin
data.list.of_fn
data.list.pairwise
data.list.perm
data.list.permutation
data.list.prod_monoid
data.list.prod_sigma
data.list.range
data.list.sort
data.list.sublists
data.list.tfae
data.list.zip
data.mllist
data.multiset.basic
data.multiset.erase_dup
data.multiset.finset_ops
data.multiset.fold
data.multiset.lattice
data.multiset.nodup
data.multiset.pi
data.multiset.powerset
data.multiset.range
data.multiset.sort
data.nat.basic
data.nat.cast
data.nat.choose.basic
data.nat.enat
data.nat.factorial.basic
data.nat.gcd
data.nat.interval
data.nat.lattice
data.nat.pairing
data.nat.pow
data.nat.sqrt
data.num.basic
data.opposite
data.option.basic
data.option.defs
data.part
data.pi
data.pnat.basic
data.pnat.interval
data.pprod
data.prod
data.quot
data.rat.basic
data.rat.cast
data.rat.floor
data.rat.meta_defs
data.rat.order
data.rbmap.basic
data.rbtree.default_lt
data.rbtree.init
data.real.basic
data.real.cau_seq
data.real.cau_seq_completion
data.real.ennreal
data.real.nnreal
data.set.basic
data.set.finite
data.set.function
data.set.intervals.basic
data.set.intervals.image_preimage
data.set.intervals.ord_connected
data.set.intervals.unordered_interval
data.set.lattice
data.set.pairwise
data.set.prod
data.set_like.basic
data.setoid.basic
data.setoid.partition
data.sigma.basic
data.string.basic
data.string.defs
data.subtype
data.sum
data.sym.basic
data.tree
data.ulift
data.vector.basic
group_theory.congruence
group_theory.coset
group_theory.group_action.basic
group_theory.group_action.defs
group_theory.group_action.group
group_theory.group_action.opposite
group_theory.group_action.pi
group_theory.group_action.prod
group_theory.group_action.sub_mul_action
group_theory.group_action.units
group_theory.perm.basic
group_theory.quotient_group
group_theory.subgroup.basic
group_theory.submonoid.basic
group_theory.submonoid.center
group_theory.submonoid.membership
group_theory.submonoid.operations
group_theory.submonoid.pointwise
linear_algebra.basic
logic.basic
logic.embedding
logic.function.basic
logic.function.conjugate
logic.function.iterate
logic.is_empty
logic.nonempty
logic.nontrivial
logic.relation
logic.relator
logic.unique
meta.expr
meta.expr_lens
meta.rb_map
order.atoms
order.basic
order.boolean_algebra
order.bounded_order
order.bounds
order.compactly_generated
order.compare
order.complete_boolean_algebra
order.complete_lattice
order.conditionally_complete_lattice
order.cover
order.directed
order.galois_connection
order.hom.basic
order.hom.lattice
order.lattice
order.lattice_intervals
order.lexicographic
order.locally_finite
order.min_max
order.modular_lattice
order.monotone
order.omega_complete_partial_order
order.order_dual
order.order_iso_nat
order.rel_classes
order.rel_iso
order.well_founded
order.zorn
ring_theory.subring.basic
ring_theory.subsemiring.basic
tactic.abel
tactic.algebra
tactic.alias
tactic.apply
tactic.apply_fun
tactic.auto_cases
tactic.binder_matching
tactic.by_contra
tactic.cache
tactic.cancel_denoms
tactic.chain
tactic.choose
tactic.clear
tactic.congr
tactic.converter.apply_congr
tactic.converter.interactive
tactic.converter.old_conv
tactic.core
tactic.dec_trivial
tactic.delta_instance
tactic.dependencies
tactic.derive_fintype
tactic.derive_inhabited
tactic.doc_commands
tactic.elide
tactic.equiv_rw
tactic.explode
tactic.ext
tactic.field_simp
tactic.fin_cases
tactic.find
tactic.finish
tactic.fix_reflect_string
tactic.generalize_proofs
tactic.generalizes
tactic.group
tactic.hint
tactic.interactive
tactic.interactive_expr
tactic.interval_cases
tactic.itauto
tactic.lean_core_docs
tactic.lift
tactic.linarith.datatypes
tactic.linarith.elimination
tactic.linarith.frontend
tactic.linarith.lemmas
tactic.linarith.parsing
tactic.linarith.preprocessing
tactic.linarith.verification
tactic.lint.basic
tactic.lint.default
tactic.lint.frontend
tactic.lint.misc
tactic.lint.simp
tactic.lint.type_classes
tactic.localized
tactic.mk_iff_of_inductive_prop
tactic.monotonicity.basic
tactic.monotonicity.interactive
tactic.monotonicity.lemmas
tactic.noncomm_ring
tactic.norm_cast
tactic.norm_num
tactic.nth_rewrite.basic
tactic.nth_rewrite.congr
tactic.nth_rewrite.default
tactic.obviously
tactic.omega.clause
tactic.omega.coeffs
tactic.omega.eq_elim
tactic.omega.find_ees
tactic.omega.find_scalars
tactic.omega.int.dnf
tactic.omega.int.form
tactic.omega.int.main
tactic.omega.int.preterm
tactic.omega.lin_comb
tactic.omega.main
tactic.omega.misc
tactic.omega.nat.dnf
tactic.omega.nat.form
tactic.omega.nat.main
tactic.omega.nat.neg_elim
tactic.omega.nat.preterm
tactic.omega.nat.sub_elim
tactic.omega.prove_unsats
tactic.omega.term
tactic.pi_instances
tactic.pretty_cases
tactic.project_dir
tactic.protected
tactic.push_neg
tactic.rcases
tactic.reassoc_axiom
tactic.rename_var
tactic.replacer
tactic.reserved_notation
tactic.restate_axiom
tactic.rewrite
tactic.ring
tactic.ring_exp
tactic.scc
tactic.show_term
tactic.simp_command
tactic.simp_result
tactic.simp_rw
tactic.simpa
tactic.simps
tactic.slice
tactic.solve_by_elim
tactic.split_ifs
tactic.squeeze
tactic.subtype_instance
tactic.suggest
tactic.tauto
tactic.tfae
tactic.tidy
tactic.transform_decl
tactic.transport
tactic.trunc_cases
tactic.unfold_cases
tactic.unify_equations
tactic.where
tactic.wlog
tactic.zify

debugger.attr

source

meta def debugger.attr :

(user_attribute unit)

General documentation

Additional documentation

Library

core

data

buffer

parser

buffer

dlist

vector

init

algebra

classes

functions

order

control

alternative

applicative

combinators

except

functor

id

lawful

lift

monad

monad_fail

option

reader

state

data

array

basic

slice

bool

basic

lemmas

char

basic

classes

lemmas

fin

basic

ops

int

basic

bitwise

comp_lemmas

order

list

basic

instances

lemmas

qsort

nat

basic

bitwise

div

gcd

lemmas

option

basic

instances

ordering

basic

lemmas

sigma

basic

lex

string

basic

ops

subtype

basic

instances

sum

basic

unsigned

basic

ops

prod

punit

quot

repr

set

setoid

to_string

lean_problem_sheets

2019

questions

sheet1

sheet2

sheet3

sheet4

solutions

sheet3

2020

functions

bijection_game

happy_animals

two_sided_inverse

univ_product

integers

int_def_solns

logic

SAT_example

bool_not

logic_lecture_ad_lib

logic_video

questions

solutions

peano

peano_practice_questions

problem_sheets

Part_II

sheet1_q3

Part_II_sheet1

relations

equiv_partition2

partition_challenge

partition_challenge_official_solution

partition_challenge_solution2

partition_challenge_xena

random_reln_transitive2

sets

canonical

real_numbers

tactic_hints

examples

2021

functions

sheet1

logic

sheet1

sheet2

sheet3

sheet4

sheet5

sheet6

sets

sheet1

sheet2

sheet3

sheet4

sheet5

sheet6

sheet7

mathlib

algebra

basic

big_operators

basic

option

order

pi

ring

field

basic

opposite

gcd_monoid

basic

group

basic

commute

conj

defs

hom

hom_instances

inj_surj

opposite

pi

prod

semiconj

to_additive

type_tags

units

units_hom

with_one

group_power

basic

lemmas

order

group_with_zero

basic

defs

power

module

basic

hom

linear_map

pi

prod

submodule

submodule_lattice

order

absolute_value

archimedean

field

floor

group

monoid

monoid_lemmas

nonneg

ring

sub

with_zero

regular

basic

smul

ring

basic

comp_typeclasses

opposite

pi

prod

star

basic

abs

associated

bounds

char_zero

covariant_and_contravariant

divisibility

euclidean_domain

field_power

free_monoid

group_action_hom

group_ring_action

indicator_function

invertible

opposites

pointwise

punit_instances

quotient

smul_with_zero

support

category_theory