mathlib
documentation
lean_problem_sheets
/
2020
.
functions
.
univ_product
Google site search
lean_problem_sheets
/
2020
.
functions
.
univ_product
source
Imports
init.default
Imported by
The Data
#
The proofs that it satisfies the axioms for product
#
the universal property
#
General documentation
index
tactics
commands
hole commands
attributes
notes
references
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
meta
converter
conv
interactive
lean
parser
smt
congruence_closure
ematch
interactive
rsimp
smt_tactic
widget
basic
html_cmd
interactive_expr
replace_save_info
tactic_component
ac_tactics
async_tactic
attribute
backward
case_tag
comp_value_tactics
congr_lemma
congr_tactic
constructor_tactic
contradiction_tactic
declaration
derive
environment
exceptional
expr
expr_address
float
format
fun_info
has_reflect
hole_command
injection_tactic
interaction_monad
interactive
interactive_base
json
level
local_context
match_tactic
mk_dec_eq_instance
mk_has_reflect_instance
mk_has_sizeof_instance
mk_inhabited_instance
module_info
name
occurrences
options
pexpr
rb_map
rec_util
ref
relation_tactics
rewrite_tactic
set_get_option_tactics
simp_tactic
tactic
tagged_format
task
type_context
vm
well_founded_tactics
cc_lemmas
classical
coe
core
default
function
funext
ite_simp
logic
propext
util
version
wf
system
io
io_interface
random
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
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
category
basic
combinatorics
quiver
control
equiv_functor
instances
monad
basic
traversable
basic
derive
equiv
lemmas
applicative
basic
bifunctor
equiv_functor
functor
data
array
lemmas
bool
all_any
basic
set
dlist
basic
equiv
encodable
basic
basic
denumerable
functor
module
mul_add
mul_add_aut
nat
ring
ring_aut
set
fin
basic
interval
finset
basic
card
fin
fold
lattice
locally_finite
option
order
pi
powerset
preimage
prod
sigma
sort
finsupp
basic
fintype
basic
card
int
basic
cast
char_zero
interval
least_greatest
list
basic
big_operators
chain
count
defs
duplicate
erase_dup
forall2
func
join
lattice
lex
min_max
nodup
nodup_equiv_fin
of_fn
pairwise
perm
permutation
prod_monoid
prod_sigma
range
sort
sublists
tfae
zip
multiset
basic
erase_dup
finset_ops
fold
lattice
nodup
pi
powerset
range
sort
nat
choose
basic
factorial
basic
basic
cast
enat
gcd
interval
lattice
pairing
pow
sqrt
num
basic
option
basic
defs
pnat
basic
interval
rat
basic
cast
floor
meta_defs
order
rbmap
basic
rbtree
default_lt
init
real
basic
cau_seq
cau_seq_completion
ennreal
nnreal
set
intervals
basic
image_preimage
ord_connected
unordered_interval
basic
finite
function
lattice
pairwise
prod
set_like
basic
setoid
basic
partition
sigma
basic
string
basic
defs
sym
basic
vector
basic
char
dfinsupp
fun_like
mllist
opposite
part
pi
pprod
prod
quot
subtype
sum
tree
ulift
group_theory
group_action
basic
defs
group
opposite
pi
prod
sub_mul_action
units
perm
basic
subgroup
basic
submonoid
basic
center
membership
operations
pointwise
congruence
coset
quotient_group
linear_algebra
basic
logic
function
basic
conjugate
iterate
basic
embedding
is_empty
nonempty
nontrivial
relation
relator
unique
meta
expr
expr_lens
rb_map
order
hom
basic
lattice
atoms
basic
boolean_algebra
bounded_order
bounds
compactly_generated
compare
complete_boolean_algebra
complete_lattice
conditionally_complete_lattice
cover
directed
galois_connection
lattice
lattice_intervals
lexicographic
locally_finite
min_max
modular_lattice
monotone
omega_complete_partial_order
order_dual
order_iso_nat
rel_classes
rel_iso
well_founded
zorn
ring_theory
subring
basic
subsemiring
basic
tactic
converter
apply_congr
interactive
old_conv
linarith
datatypes
elimination
frontend
lemmas
parsing
preprocessing
verification
lint
basic
default
frontend
misc
simp
type_classes
monotonicity
basic
interactive
lemmas
nth_rewrite
basic
congr
default
omega
int
dnf
form
main
preterm
nat
dnf
form
main
neg_elim
preterm
sub_elim
clause
coeffs
eq_elim
find_ees
find_scalars
lin_comb
main
misc
prove_unsats
term
abel
algebra
alias
apply
apply_fun
auto_cases
binder_matching
by_contra
cache
cancel_denoms
chain
choose
clear
congr
core
dec_trivial
delta_instance
dependencies
derive_fintype
derive_inhabited
doc_commands
elide
equiv_rw
explode
ext
field_simp
fin_cases
find
finish
fix_reflect_string
generalize_proofs
generalizes
group
hint
interactive
interactive_expr
interval_cases
itauto
lean_core_docs
lift
localized
mk_iff_of_inductive_prop
noncomm_ring
norm_cast
norm_num
obviously
pi_instances
pretty_cases
project_dir
protected
push_neg
rcases
reassoc_axiom
rename_var
replacer
reserved_notation
restate_axiom
rewrite
ring
ring_exp
scc
show_term
simp_command
simp_result
simp_rw
simpa
simps
slice
solve_by_elim
split_ifs
squeeze
subtype_instance
suggest
tauto
tfae
tidy
transform_decl
transport
trunc_cases
unfold_cases
unify_equations
where
wlog
zify