Documentation

Mathlib.Init.Align

Realignments from lean 3 init #

These are collected in one place only for ease of maintenance of a bunch of files that would otherwise be nothing but #aligns. Please use the respective files in Mathlib.Init if there are actual theorems in the files.

init.algebra.classes #

init.cc_lemmas #

init.classical #

init.coe #

init.control.alternative #

init.control.applicative #

init.control.except #

init.control.functor #

init.control.lift #

init.control.monad #

init.data.array.default #

init.data.char.basic #

init.data.char.classes #

init.data.char.default #

init.data.default #

init.data.fin.basic #

init.data.int.comp_lemmas #

init.data.int.default #

init.data.list.basic #

init.data.nat.basic #

init.data.nat.div #

init.data.nat.lemmas #

init.data.option.instances #

init.data.ordering.basic #

init.data.prod #

init.data.punit #

init.data.quot #

init.data.random #

init.data.repr #

init.data.setoid #

init.data.sigma.basic #

init.data.string.basic #

init.data.subtype.basic #

init.data.sum.basic #

init.data.sum.default #

init.data.to_string #

init.data.unsigned.basic #

init.data.unsigned.default #

init.default #

init.function #

init.funext #

init.meta.exceptional #

init.meta.float #

init.meta.format #

init.meta.json #

init.meta.level #

init.meta.name #

init.meta.options #

init.meta.rb_map #

init.meta.task #

init.meta.widget.basic #

init.meta.widget.default #

init.meta.widget.html_cmd #

init.meta.widget.interactive_expr #

init.meta.widget.replace_save_info #

init.meta.widget.tactic_component #

init.prelude #

init.propext #

init.util #

init.version #

init.wf #