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.feature_search
init.meta.float
init.meta.well_founded_tactics
init.propext
init.util
init.version
init.wf

Imported by

data.buffer
data.dlist
system.io
system.io_interface
system.random
adeles_R
adeles_function_field
adeles_number_field
examples
fractional_ideal
function_field
galois
ideles_R
ideles_function_field
ideles_number_field
main_theorem_GCFT
valuation
algebra.abs
algebra.algebra.basic
algebra.algebra.bilinear
algebra.algebra.operations
algebra.algebra.restrict_scalars
algebra.algebra.subalgebra.basic
algebra.algebra.subalgebra.pointwise
algebra.algebra.tower
algebra.associated
algebra.big_operators.associated
algebra.big_operators.basic
algebra.big_operators.fin
algebra.big_operators.finprod
algebra.big_operators.finsupp
algebra.big_operators.intervals
algebra.big_operators.multiset
algebra.big_operators.nat_antidiagonal
algebra.big_operators.option
algebra.big_operators.order
algebra.big_operators.pi
algebra.big_operators.ring
algebra.bounds
algebra.category.CommRing.basic
algebra.category.Group.basic
algebra.category.Mon.basic
algebra.char_p.basic
algebra.char_p.two
algebra.char_zero
algebra.covariant_and_contravariant
algebra.direct_limit
algebra.direct_sum.basic
algebra.direct_sum.finsupp
algebra.direct_sum.module
algebra.divisibility
algebra.euclidean_domain
algebra.field.basic
algebra.field.opposite
algebra.field_power
algebra.free_monoid
algebra.gcd_monoid.basic
algebra.gcd_monoid.finset
algebra.gcd_monoid.multiset
algebra.geom_sum
algebra.group.basic
algebra.group.commute
algebra.group.conj
algebra.group.defs
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.with_one
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.hom.aut
algebra.hom.equiv
algebra.hom.group
algebra.hom.group_action
algebra.hom.group_instances
algebra.hom.iterate
algebra.hom.non_unital_alg
algebra.hom.units
algebra.indicator_function
algebra.invertible
algebra.is_prime_pow
algebra.module.basic
algebra.module.equiv
algebra.module.hom
algebra.module.linear_map
algebra.module.opposites
algebra.module.pi
algebra.module.prod
algebra.module.submodule
algebra.module.submodule_lattice
algebra.module.submodule_pointwise
algebra.monoid_algebra.basic
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.parity
algebra.periodic
algebra.polynomial.big_operators
algebra.polynomial.group_ring_action
algebra.punit_instances
algebra.quotient
algebra.regular.basic
algebra.regular.smul
algebra.ring.aut
algebra.ring.basic
algebra.ring.comp_typeclasses
algebra.ring.equiv
algebra.ring.opposite
algebra.ring.pi
algebra.ring.prod
algebra.smul_with_zero
algebra.squarefree
algebra.star.basic
algebra.star.pi
algebra.support
algebraic_geometry.prime_spectrum.basic
algebraic_geometry.prime_spectrum.noetherian
category_theory.adjunction.basic
category_theory.category.basic
category_theory.concrete_category.basic
category_theory.concrete_category.bundled
category_theory.concrete_category.bundled_hom
category_theory.concrete_category.reflects_isomorphisms
category_theory.endomorphism
category_theory.epi_mono
category_theory.eq_to_hom
category_theory.equivalence
category_theory.essential_image
category_theory.full_subcategory
category_theory.functor.basic
category_theory.functor.category
category_theory.functor.fully_faithful
category_theory.functor.reflects_isomorphisms
category_theory.groupoid
category_theory.isomorphism
category_theory.natural_isomorphism
category_theory.natural_transformation
category_theory.opposites
category_theory.pi.basic
category_theory.products.basic
category_theory.types
category_theory.whiskering
combinatorics.composition
combinatorics.partition
combinatorics.quiver.basic
control.applicative
control.basic
control.bifunctor
control.equiv_functor
control.functor
control.monad.basic
control.traversable.basic
control.traversable.derive
control.traversable.equiv
control.traversable.instances
control.traversable.lemmas
data.array.lemmas
data.bool.all_any
data.bool.basic
data.bool.set
data.bracket
data.char
data.complex.basic
data.dfinsupp.basic
data.dlist.basic
data.fin.basic
data.fin.interval
data.fin.tuple.basic
data.fin.vec_notation
data.finset.basic
data.finset.card
data.finset.fin
data.finset.finsupp
data.finset.fold
data.finset.lattice
data.finset.locally_finite
data.finset.nat_antidiagonal
data.finset.noncomm_prod
data.finset.option
data.finset.order
data.finset.pairwise
data.finset.pi
data.finset.pointwise
data.finset.powerset
data.finset.preimage
data.finset.prod
data.finset.sigma
data.finset.sort
data.finsupp.antidiagonal
data.finsupp.basic
data.finsupp.indicator
data.finsupp.interval
data.finsupp.multiset
data.finsupp.order
data.finsupp.pwo
data.finsupp.to_dfinsupp
data.fintype.basic
data.fintype.card
data.fintype.fin
data.fintype.sort
data.fun_like.basic
data.fun_like.embedding
data.fun_like.equiv
data.int.basic
data.int.cast
data.int.char_zero
data.int.gcd
data.int.interval
data.int.least_greatest
data.int.modeq
data.int.order
data.int.parity
data.int.succ_pred
data.list.basic
data.list.big_operators
data.list.chain
data.list.count
data.list.dedup
data.list.defs
data.list.duplicate
data.list.forall2
data.list.infix
data.list.join
data.list.lattice
data.list.lex
data.list.min_max
data.list.nat_antidiagonal
data.list.nodup
data.list.nodup_equiv_fin
data.list.of_fn
data.list.pairwise
data.list.perm
data.list.permutation
data.list.prime
data.list.range
data.list.rotate
data.list.sort
data.list.sublists
data.list.tfae
data.list.zip
data.matrix.basic
data.matrix.basis
data.matrix.block
data.matrix.char_p
data.matrix.dmatrix
data.matrix.pequiv
data.mllist
data.multiset.antidiagonal
data.multiset.basic
data.multiset.bind
data.multiset.dedup
data.multiset.finset_ops
data.multiset.fold
data.multiset.lattice
data.multiset.nat_antidiagonal
data.multiset.nodup
data.multiset.pi
data.multiset.powerset
data.multiset.range
data.multiset.sort
data.mv_polynomial.basic
data.mv_polynomial.comm_ring
data.mv_polynomial.equiv
data.mv_polynomial.monad
data.mv_polynomial.rename
data.mv_polynomial.variables
data.nat.basic
data.nat.cast
data.nat.choose.basic
data.nat.choose.dvd
data.nat.choose.sum
data.nat.count
data.nat.enat
data.nat.factorial.basic
data.nat.factorization
data.nat.gcd
data.nat.interval
data.nat.lattice
data.nat.modeq
data.nat.pairing
data.nat.parity
data.nat.periodic
data.nat.pow
data.nat.prime
data.nat.sqrt
data.nat.sqrt_norm_num
data.nat.succ_pred
data.nat.totient
data.nat.with_bot
data.num.basic
data.opposite
data.option.basic
data.option.defs
data.part
data.pequiv
data.pfun
data.pi
data.pnat.basic
data.pnat.interval
data.polynomial.algebra_map
data.polynomial.basic
data.polynomial.cancel_leads
data.polynomial.coeff
data.polynomial.degree.definitions
data.polynomial.degree.lemmas
data.polynomial.degree.trailing_degree
data.polynomial.derivative
data.polynomial.div
data.polynomial.erase_lead
data.polynomial.eval
data.polynomial.field_division
data.polynomial.induction
data.polynomial.inductions
data.polynomial.integral_normalization
data.polynomial.monic
data.polynomial.monomial
data.polynomial.reverse
data.polynomial.ring_division
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.real.sqrt
data.rel
data.set.Union_lift
data.set.accumulate
data.set.basic
data.set.countable
data.set.finite
data.set.function
data.set.functor
data.set.intervals.basic
data.set.intervals.disjoint
data.set.intervals.image_preimage
data.set.intervals.ord_connected
data.set.intervals.pi
data.set.intervals.unordered_interval
data.set.lattice
data.set.pairwise
data.set.pointwise
data.set.prod
data.set.sigma
data.set_like.basic
data.setoid.basic
data.sigma.basic
data.string.basic
data.string.defs
data.subtype
data.sum.basic
data.sum.order
data.sym.basic
data.tree
data.ulift
data.vector.basic
data.zmod.algebra
data.zmod.basic
dynamics.fixed_points.basic
dynamics.periodic_pts
field_theory.adjoin
field_theory.finite.basic
field_theory.finiteness
field_theory.fixed
field_theory.galois
field_theory.intermediate_field
field_theory.is_alg_closed.algebraic_closure
field_theory.is_alg_closed.basic
field_theory.krull_topology
field_theory.minpoly
field_theory.normal
field_theory.perfect_closure
field_theory.primitive_element
field_theory.ratfunc
field_theory.separable
field_theory.splitting_field
field_theory.subfield
field_theory.tower
group_theory.abelianization
group_theory.archimedean
group_theory.commutator
group_theory.congruence
group_theory.coset
group_theory.exponent
group_theory.finiteness
group_theory.free_abelian_group
group_theory.free_group
group_theory.group_action.basic
group_theory.group_action.big_operators
group_theory.group_action.conj_act
group_theory.group_action.defs
group_theory.group_action.fixing_subgroup
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.monoid_localization
group_theory.order_of_element
group_theory.perm.basic
group_theory.perm.cycle_type
group_theory.perm.cycles
group_theory.perm.fin
group_theory.perm.option
group_theory.perm.sign
group_theory.perm.subgroup
group_theory.perm.support
group_theory.quotient_group
group_theory.solvable
group_theory.specific_groups.cyclic
group_theory.subgroup.basic
group_theory.subgroup.pointwise
group_theory.submonoid.basic
group_theory.submonoid.center
group_theory.submonoid.centralizer
group_theory.submonoid.inverses
group_theory.submonoid.membership
group_theory.submonoid.operations
group_theory.submonoid.pointwise
group_theory.subsemigroup.basic
linear_algebra.alternating
linear_algebra.basic
linear_algebra.basis
linear_algebra.bilinear_form
linear_algebra.bilinear_map
linear_algebra.charpoly.basic
linear_algebra.contraction
linear_algebra.determinant
linear_algebra.dfinsupp
linear_algebra.dimension
linear_algebra.direct_sum.finsupp
linear_algebra.direct_sum.tensor_product
linear_algebra.dual
linear_algebra.finite_dimensional
linear_algebra.finsupp
linear_algebra.finsupp_vector_space
linear_algebra.free_module.basic
linear_algebra.free_module.finite.basic
linear_algebra.free_module.finite.rank
linear_algebra.free_module.rank
linear_algebra.free_module.strong_rank_condition
linear_algebra.invariant_basis_number
linear_algebra.isomorphisms
linear_algebra.linear_independent
linear_algebra.linear_pmap
linear_algebra.matrix.adjugate
linear_algebra.matrix.basis
linear_algebra.matrix.bilinear_form
linear_algebra.matrix.charpoly.basic
linear_algebra.matrix.charpoly.coeff
linear_algebra.matrix.determinant
linear_algebra.matrix.finite_dimensional
linear_algebra.matrix.mv_polynomial
linear_algebra.matrix.nondegenerate
linear_algebra.matrix.nonsingular_inverse
linear_algebra.matrix.polynomial
linear_algebra.matrix.reindex
linear_algebra.matrix.to_lin
linear_algebra.matrix.to_linear_equiv
linear_algebra.matrix.trace
linear_algebra.multilinear.basic
linear_algebra.multilinear.basis
linear_algebra.multilinear.tensor_product
linear_algebra.pi
linear_algebra.prod
linear_algebra.projection
linear_algebra.quotient
linear_algebra.sesquilinear_form
linear_algebra.span
linear_algebra.std_basis
linear_algebra.tensor_product
linear_algebra.tensor_product_basis
linear_algebra.trace
linear_algebra.vandermonde
logic.basic
logic.denumerable
logic.embedding
logic.encodable.basic
logic.encodable.lattice
logic.equiv.basic
logic.equiv.fin
logic.equiv.fintype
logic.equiv.functor
logic.equiv.list
logic.equiv.nat
logic.equiv.option
logic.equiv.set
logic.function.basic
logic.function.conjugate
logic.function.iterate
logic.is_empty
logic.nonempty
logic.nontrivial
logic.relation
logic.relator
logic.small
logic.unique
meta.expr
meta.expr_lens
meta.rb_map
number_theory.divisors
number_theory.function_field
number_theory.legendre_symbol.gauss_eisenstein_lemmas
number_theory.legendre_symbol.quadratic_reciprocity
number_theory.number_field
number_theory.padics.padic_norm
number_theory.zsqrtd.basic
number_theory.zsqrtd.gaussian_int
order.antichain
order.atoms
order.basic
order.boolean_algebra
order.bounded
order.bounded_order
order.bounds
order.chain
order.compactly_generated
order.compare
order.complete_boolean_algebra
order.complete_lattice
order.complete_lattice_intervals
order.conditionally_complete_lattice
order.copy
order.cover
order.directed
order.filter.archimedean
order.filter.at_top_bot
order.filter.bases
order.filter.basic
order.filter.cofinite
order.filter.interval
order.filter.lift
order.filter.n_ary
order.filter.partial
order.filter.pi
order.filter.pointwise
order.filter.ultrafilter
order.fixed_points
order.galois_connection
order.hom.basic
order.hom.bounded
order.hom.complete_lattice
order.hom.lattice
order.hom.order
order.iterate
order.lattice
order.lattice_intervals
order.lexicographic
order.locally_finite
order.max
order.min_max
order.modular_lattice
order.monotone
order.omega_complete_partial_order
order.order_dual
order.order_iso_nat
order.partial_sups
order.pilex
order.rel_classes
order.rel_iso
order.succ_pred.basic
order.succ_pred.relation
order.sup_indep
order.symm_diff
order.well_founded
order.well_founded_set
order.zorn
ring_theory.adjoin.basic
ring_theory.adjoin.fg
ring_theory.adjoin_root
ring_theory.algebra_tower
ring_theory.algebraic
ring_theory.class_group
ring_theory.coprime.basic
ring_theory.coprime.lemmas
ring_theory.dedekind_domain.basic
ring_theory.dedekind_domain.ideal
ring_theory.dedekind_domain.integral_closure
ring_theory.euclidean_domain
ring_theory.finiteness
ring_theory.fractional_ideal
ring_theory.free_comm_ring
ring_theory.free_ring
ring_theory.hahn_series
ring_theory.ideal.basic
ring_theory.ideal.local_ring
ring_theory.ideal.operations
ring_theory.ideal.over
ring_theory.ideal.prod
ring_theory.ideal.quotient
ring_theory.int.basic
ring_theory.integral_closure
ring_theory.integral_domain
ring_theory.integrally_closed
ring_theory.laurent_series
ring_theory.localization.at_prime
ring_theory.localization.away
ring_theory.localization.basic
ring_theory.localization.fraction_ring
ring_theory.localization.ideal
ring_theory.localization.integer
ring_theory.localization.integral
ring_theory.localization.num_denom
ring_theory.localization.submodule
ring_theory.matrix_algebra
ring_theory.multiplicity
ring_theory.nilpotent
ring_theory.noetherian
ring_theory.non_zero_divisors
ring_theory.polynomial.basic
ring_theory.polynomial.content
ring_theory.polynomial.gauss_lemma
ring_theory.polynomial.rational_root
ring_theory.polynomial.scale_roots
ring_theory.polynomial.tower
ring_theory.polynomial_algebra
ring_theory.power_basis
ring_theory.power_series.basic
ring_theory.principal_ideal_domain
ring_theory.subring.basic
ring_theory.subring.pointwise
ring_theory.subsemiring.basic
ring_theory.subsemiring.pointwise
ring_theory.tensor_product
ring_theory.trace
ring_theory.unique_factorization_domain
ring_theory.valuation.basic
ring_theory.valuation.integers
set_theory.cardinal.basic
set_theory.cardinal.cofinality
set_theory.cardinal.finite
set_theory.cardinal.ordinal
set_theory.ordinal.arithmetic
set_theory.ordinal.basic
set_theory.ordinal.principal
set_theory.schroeder_bernstein
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_inhabited
tactic.doc_commands
tactic.elementwise
tactic.elide
tactic.explode
tactic.ext
tactic.field_simp
tactic.fin_cases
tactic.find
tactic.finish
tactic.fix_reflect_string
tactic.fresh_names
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.norm_cast
tactic.norm_fin
tactic.norm_num
tactic.norm_swap
tactic.nth_rewrite.basic
tactic.nth_rewrite.congr
tactic.nth_rewrite.default
tactic.obviously
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.suggest
tactic.tauto
tactic.tfae
tactic.tidy
tactic.transform_decl
tactic.trunc_cases
tactic.unify_equations
tactic.where
tactic.with_local_reducibility
tactic.wlog
tactic.zify
topology.algebra.const_mul_action
topology.algebra.constructions
topology.algebra.field
topology.algebra.filter_basis
topology.algebra.group
topology.algebra.group_completion
topology.algebra.group_with_zero
topology.algebra.infinite_sum
topology.algebra.localization
topology.algebra.module.basic
topology.algebra.monoid
topology.algebra.mul_action
topology.algebra.nonarchimedean.bases
topology.algebra.nonarchimedean.basic
topology.algebra.open_subgroup
topology.algebra.order.basic
topology.algebra.order.compact
topology.algebra.order.intermediate_value
topology.algebra.order.left_right
topology.algebra.order.monotone_continuity
topology.algebra.order.monotone_convergence
topology.algebra.ring
topology.algebra.uniform_field
topology.algebra.uniform_filter_basis
topology.algebra.uniform_group
topology.algebra.uniform_ring
topology.algebra.valuation
topology.algebra.valued_field
topology.algebra.with_zero_topology
topology.bases
topology.basic
topology.bornology.basic
topology.compact_open
topology.connected
topology.constructions
topology.continuous_function.basic
topology.continuous_on
topology.dense_embedding
topology.homeomorph
topology.instances.int
topology.instances.nnreal
topology.instances.real
topology.maps
topology.metric_space.basic
topology.metric_space.emetric_space
topology.nhds_set
topology.order
topology.separation
topology.sets.closeds
topology.sets.compacts
topology.sets.opens
topology.sober
topology.subset_properties
topology.support
topology.tactic
topology.uniform_space.abstract_completion
topology.uniform_space.basic
topology.uniform_space.cauchy
topology.uniform_space.complete_separated
topology.uniform_space.completion
topology.uniform_space.pi
topology.uniform_space.separation
topology.uniform_space.uniform_convergence
topology.uniform_space.uniform_embedding

debugger.attr

source

meta def debugger.attr :

(user_attribute unit)

General documentation

Additional documentation

Library

core

data

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

ideles

adeles_R

adeles_function_field

adeles_number_field

examples

fractional_ideal

function_field

galois

ideles_R

ideles_function_field

ideles_number_field

main_theorem_GCFT

valuation

mathlib

algebra

subalgebra

basic

pointwise

basic

bilinear

operations

restrict_scalars

tower

big_operators

associated

basic

fin

finprod

finsupp

intervals

multiset

nat_antidiagonal

option

order

pi

ring

Color scheme

dark system light