mathlib
documentation
data
.
pprod
Google site search
data
.
pprod
source
Imports
init.default
Imported by
pprod
.
mk
.
eta
Extra facts about
pprod
#
source
@[simp]
theorem
pprod
.
mk
.
eta
{α : Sort u_1}
{β : Sort u_2}
{p :
pprod
α
β}
:
⟨
p.
fst
, p.
snd
⟩
=
p
General documentation
index
tactics
commands
hole commands
attributes
notes
references
Additional documentation
mathlib overview
tactic writing
calc mode
conv mode
simplification
well founded recursion
style guide
documentation style guide
naming conventions
Library
src
export_json
core
data
buffer
parser
buffer
dlist
lazy_list
stream
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
rbmap
basic
rbtree
basic
default
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
mathlib
algebra
algebra
basic
operations
ordered
subalgebra
tower
big_operators
basic
enat
fin
finprod
finsupp
intervals
nat_antidiagonal
order
pi
ring
category
Algebra
basic
limits
CommRing
adjunctions
basic
colimits
limits
Group
Z_Module_equivalence
abelian
adjunctions
basic
biproducts
colimits
images
limits
preadditive
subobject
zero
Module
abelian
adjunctions
basic
colimits
epi_mono
kernels
limits
monoidal
subobject
Mon
adjunctions
basic
colimits
limits
Semigroup
basic
char_p
basic
exp_char
invertible
pi
quotient
subring
continued_fractions
computation
approximation_corollaries
approximations
basic
correctness_terminating
default
terminates_iff_rat
translations
basic
continuants_recurrence
convergents_equiv
default
terminated_stable
translations
group
basic
commute
conj
default
defs
hom
hom_instances
inj_surj
pi
prod
semiconj
to_additive
type_tags
ulift
units
units_hom
with_one
group_power
basic
identities
lemmas
order
group_with_zero
basic
defs
power
homology
chain_complex
exact
homology
image_to_kernel_map
lie
abelian
basic
cartan_subalgebra
character
classical
direct_sum
ideal_operations
matrix
nilpotent
of_associative
quotient
semisimple
skew_adjoint
solvable
subalgebra
submodule
tensor_product
universal_enveloping
weights
module
basic
default
hom
linear_map
opposites
ordered
pi
prod
projective
submodule
submodule_lattice
ulift
polynomial
big_operators
group_ring_action
ring
basic
boolean_ring
default
pi
prod
ulift
star
algebra
basic
chsh
pi
add_torsor
archimedean
associated
char_zero
direct_limit
direct_sum
direct_sum_graded
divisibility
euclidean_domain
field
field_power
floor
free
free_algebra
free_monoid
gcd_monoid
geom_sum
group_action_hom
group_ring_action
hierarchy_design
invertible
iterate_hom
linear_ordered_comm_group_with_zero
linear_recurrence
monoid_algebra
monoid_algebra_to_direct_sum
opposites
order
order_functions
ordered_field
ordered_group
ordered_monoid
ordered_pi
ordered_ring
pempty_instances
pointwise
punit_instances
quadratic_discriminant
quandle
regular
ring_quot
smul_regular
smul_with_zero
squarefree
triv_sq_zero_ext
algebraic_geometry
presheafed_space
has_colimits
Scheme
Spec
is_open_comap_C
locally_ringed_space
presheafed_space
prime_spectrum
sheafed_space
stalks
structure_sheaf
algebraic_topology
simplex_category
simplicial_object
simplicial_set
analysis
ODE
gronwall
analytic
basic
composition
inverse
linear
radius_liminf
asymptotics
asymptotic_equivalent
asymptotics
specific_asymptotics
calculus
darboux
deriv
extend_deriv
fderiv
fderiv_measurable
formal_multilinear_series
implicit
inverse
iterated_deriv
lagrange_multipliers
lhopital
local_extr
mean_value
specific_functions
tangent_cone
times_cont_diff
complex
basic
polynomial
real_deriv
roots_of_unity
convex
basic
caratheodory
cone
extrema
extreme
integral
specific_functions
topology
normed_space
add_torsor
banach
basic
bounded_linear_maps
complemented
dual
enorm
euclidean_dist
extend
finite_dimension
hahn_banach
indicator_function
inner_product
linear_isometry
mazur_ulam
multilinear
normed_group_hom
operator_norm
ordered
riesz_lemma
units
special_functions
arsinh
bernstein
exp_log
integrals
polynomials
pow
sqrt
trigonometric
hofer
mean_inequalities
p_series
quaternion
seminorm
specific_limits
category_theory
abelian
diagram_lemmas
four
basic
exact
non_preadditive
opposite
projective
pseudoelements
additive
basic
adjunction
basic
fully_faithful
lifting
limits
mates
opposites
over
reflective
category
Cat
Groupoid
Kleisli
Quiv
Rel
default
pairwise
ulift
closed
cartesian
functor
monoidal
types
zero
concrete_category
basic
bundled
bundled_hom
reflects_isomorphisms
unbundled_hom
enriched
basic
limits
constructions
over
connected
default
products
binary_products
epi_mono
equalizers
finite_products_of_binary_products
limits_of_products_and_equalizers
pullbacks
preserves
shapes
binary_products
equalizers
products
pullbacks
terminal
basic
functor_category
limits
shapes
binary_products
biproducts
concrete_category
equalizers
finite_limits
finite_products
images
kernel_pair
kernels
normal_mono
products
pullbacks
reflexive
regular_mono
split_coequalizer
strong_epi
terminal
types
wide_pullbacks
zero
cofinal
colimit_limit
concrete_category
cones
connected
creates
filtered_colimit_commutes_finite_limit
fubini
functor_category
has_limits
is_limit
kan_extension
lattice
opposites
over
pi
presheaf
punit
small_complete
types
yoneda
linear
default
linear_functor
monad
adjunction
algebra
basic
coequalizer
equiv_mon
kleisli
limits
monadicity
products
types
monoidal
free
basic
coherence
internal
Module
functor_category
limits
types
CommMon_
End
Mod
Mon_
braided
category
center
discrete
functor
functor_category
functorial
limits
natural_transformation
of_chosen_finite_products
of_has_finite_products
skeleton
transport
types
pi
basic
preadditive
Mat
additive_functor
biproducts
default
opposite
schur
single_obj
products
associator
basic
bifunctor
sigma
basic
sites
canonical
closed
grothendieck
pretopology
sheaf
sheaf_of_types
sieves
spaces
types
subobject
basic
factor_thru
lattice
limits
mono_over
types
well_powered
sums
associator
basic
triangulated
basic
pretriangulated
rotate
Fintype
action
arrow
comma
conj
connected_components
const
core
currying
differential_object
discrete_category
elements
endomorphism
epi_mono
eq_to_hom
equivalence
essential_image
essentially_small
filtered
fin_category
full_subcategory
fully_faithful
functor
functor_category
functorial
graded_object
grothendieck
groupoid
hom_functor
is_connected
isomorphism
isomorphism_classes
lifting_properties
natural_isomorphism
natural_transformation
opposites
over
path_category
pempty
punit
quotient
reflects_isomorphisms
shift
simple
single_obj
skeletal
structured_arrow
subterminal
thin
types
whiskering
with_terminal
yoneda
combinatorics
simple_graph
adj_matrix
basic
degree_sum
matching
strongly_regular
colex
composition
hall
partition
pigeonhole
quiver
computability
DFA
NFA
encoding
epsilon_NFA
halting
language
partrec
partrec_code
primrec
reduce
regular_expressions
tm_computable
tm_to_partrec
turing_machine
control
bitraversable
basic
instances
lemmas
equiv_functor
instances
functor
multivariate
monad
basic
cont
writer
traversable
basic
derive
equiv
instances
lemmas
applicative
basic
bifunctor
equiv_functor
fix
fold
functor
lawful_fix
uliftable
data
analysis
filter
topology
array
lemmas
bitvec
basic
core
buffer
parser
basic
numeral
basic
complex
basic
exponential
exponential_bounds
is_R_or_C
module
dlist
basic
instances
equiv
encodable
basic
lattice
basic
denumerable
fin
fintype
functor
list
local_equiv
mul_add
mul_add_aut
nat
option
ring
ring_aut
transfer_instance
finset
basic
fold
gcd
intervals
lattice
nat_antidiagonal
order
pi
powerset
preimage
sort
finsupp
basic
default
lattice
pointwise
to_dfinsupp
fintype
basic
card
fin
intervals
sort
fp
basic
int
basic
cast
char_zero
gcd
modeq
nat_prime
parity
range
sqrt
lazy_list
basic
list
alist
bag_inter
basic
chain
defs
erase_dup
forall2
func
indexes
intervals
min_max
nat_antidiagonal
nodup
nodup_equiv_fin
of_fn
pairwise
palindrome
perm
range
rotate
sections
sigma
sort
tfae
zip
matrix
basic
char_p
dmatrix
notation
pequiv
multiset
antidiagonal
basic
erase_dup
finset_ops
fold
functor
gcd
intervals
lattice
nat_antidiagonal
nodup
pi
powerset
range
sections
sort
mv_polynomial
basic
comap
comm_ring
counit
equiv
expand
funext
invertible
monad
pderiv
rename
variables
nat
choose
basic
dvd
sum
basic
bitwise
cast
digits
dist
enat
factorial
fib
gcd
log
modeq
multiplicity
pairing
parity
prime
psub
sqrt
totient
upto
with_bot
num
basic
bitwise
lemmas
prime
option
basic
defs
ordmap
ordnode
ordset
padics
hensel
padic_integers
padic_norm
padic_numbers
ring_homs
pfunctor
multivariate
M
W
basic
univariate
M
basic
pnat
basic
factors
intervals
prime
xgcd
polynomial
degree
definitions
lemmas
trailing_degree
algebra_map
basic
cancel_leads
coeff
denoms_clearable
derivative
div
erase_lead
eval
field_division
identities
induction
integral_normalization
iterated_deriv
lifts
mirror
monic
monomial
reverse
ring_division
qpf
multivariate
constructions
cofix
comp
const
fix
prj
quot
sigma
basic
univariate
basic
rat
basic
cast
default
denumerable
floor
meta_defs
order
sqrt
real
basic
cardinality
cau_seq
cau_seq_completion
conjugate_exponents
ennreal
ereal
golden_ratio
hyperreal
irrational
liouville
nnreal
pi
sqrt
seq
computation
parallel
seq
wseq
set
intervals
basic
disjoint
image_preimage
infinite
ord_connected
pi
proj_Icc
surj_on
unordered_interval
accumulate
basic
constructions
countable
disjointed
enumerate
finite
function
lattice
setoid
basic
partition
sigma
basic
stream
basic
string
basic
defs
zmod
basic
parity
zsqrtd
basic
gaussian_int
to_real
W
bool
bracket
char
dfinsupp
erased
fin
fin2
fin_enum
fincard
finmap
hash_map
holor
indicator_function
mllist
opposite
pequiv
pfun
pi
pprod
prod
quaternion
quot
rel
semiquot
set_like
subtype
sum
support
sym
sym2
tprod
tree
typevec
ulift
vector2
deprecated
group
ring
subfield
subgroup
submonoid
subring
dynamics
circle
rotation_number
translation_number
ergodic
conservative
measure_preserving
fixed_points
basic
topology
flow
omega_limit
periodic_pts
field_theory
finite
basic
polynomial
abel_ruffini
adjoin
algebraic_closure
chevalley_warning
fixed
galois
intermediate_field
minpoly
mv_polynomial
normal
perfect_closure
polynomial_galois_group
primitive_element
separable
separable_degree
splitting_field
subfield
tower
geometry
euclidean
basic
circumcenter
monge_point
sphere
triangle
manifold
algebra
lie_group
monoid
smooth_functions
structures
instances
circle
real
sphere
units_of_normed_algebra
basic_smooth_bundle
bump_function
charted_space
diffeomorph
local_invariant_properties
mfderiv
smooth_manifold_with_corners
times_cont_mdiff
times_cont_mdiff_map
group_theory
group_action
basic
defs
group
prod
sub_mul_action
perm
basic
cycle_type
cycles
fin
option
sign
subgroup
support
specific_groups
alternating
cyclic
dihedral
quaternion
submonoid
basic
membership
operations
abelianization
archimedean
congruence
coset
eckmann_hilton
finiteness
free_abelian_group
free_group
is_free_group
monoid_localization
nielsen_schreier
order_of_element
presented_group
quotient_group
semidirect_product
solvable
subgroup
sylow
linear_algebra
affine_space
affine_equiv
affine_map
affine_subspace
basic
combination
finite_dimensional
independent
midpoint
ordered
char_poly
basic
coeff
clifford_algebra
basic
conjugation
direct_sum
finsupp
tensor_product
adic_completion
alternating
basic
basis
bilinear_form
contraction
determinant
dfinsupp
dimension
direct_sum_module
dual
eigenspace
exterior_algebra
finite_dimensional
finsupp
finsupp_vector_space
free_algebra
free_module
invariant_basis_number
lagrange
linear_independent
linear_pmap
matrix
multilinear
nonsingular_inverse
pi
pi_tensor_product
prod
projection
quadratic_form
sesquilinear_form
smodeq
special_linear_group
std_basis
tensor_algebra
tensor_product
unitary_group
vandermonde
logic
function
basic
conjugate
iterate
basic
embedding
girard
nontrivial
relation
relator
small
unique
measure_theory
category
Meas
ae_eq_fun
ae_measurable_sequence
arithmetic
bochner_integration
borel_space
content
decomposition
ess_sup
giry_monad
group
haar_measure
hausdorff_measure
integration
interval_integral
l1_space
l2_space
lebesgue_measure
lp_space
measurable_space
measure_space
outer_measure
pi
pi_system
probability_mass_function
prod
prod_group
set_integral
simple_func_dense
meta
coinductive_predicates
expr
expr_lens
rb_map
uchange
number_theory
ADE_inequality
arithmetic_function
basic
bernoulli
bernoulli_polynomials
dioph
divisors
fermat4
lucas_lehmer
pell
primes_congruent_one
primorial
pythagorean_triples
quadratic_reciprocity
sum_four_squares
sum_two_squares
order
category
LinearOrder
NonemptyFinLinOrd
PartialOrder
Preorder
omega_complete_partial_order
filter
archimedean
at_top_bot
bases
basic
cofinite
countable_Inter
ennreal
extr
filter_product
germ
indicator_function
interval
lift
partial
pointwise
ultrafilter
atoms
basic
boolean_algebra
bounded_lattice
bounds
closure
compactly_generated
complete_boolean_algebra
complete_lattice
conditionally_complete_lattice
copy
countable_dense_linear_order
directed
extension
fixed_points
galois_connection
ideal
iterate
lattice
lattice_intervals
lexicographic
liminf_limsup
modular_lattice
omega_complete_partial_order
ord_continuous
order_dual
order_iso_nat
pfilter
pilex
preorder_hom
prime_ideal
rel_classes
rel_iso
semiconj_Sup
well_founded
well_founded_set
zorn
probability_theory
independence
integration
representation_theory
maschke
ring_theory
adjoin
basic
power_basis
ideal
basic
operations
over
prod
int
basic
mv_polynomial
basic
polynomial
basic
bernstein
chebyshev
content
cyclotomic
dickson
gauss_lemma
homogeneous
pochhammer
rational_root
scale_roots
symmetric
tower
vieta
power_series
basic
well_known
valuation
basic
integers
integral
witt_vector
basic
compare
defs
frobenius
identities
init_tail
is_poly
mul_p
structure_polynomial
teichmuller
truncated
verschiebung
witt_polynomial
adjoin_root
algebra_tower
algebraic
coprime
dedekind_domain
derivation
discrete_valuation_ring
eisenstein_criterion
euclidean_domain
finiteness
fintype
flat
fractional_ideal
free_comm_ring
free_ring
hahn_series
integral_closure
integral_domain
jacobson
jacobson_ideal
localization
matrix_algebra
multiplicity
noetherian
non_zero_divisors
nullstellensatz
perfection
polynomial_algebra
power_basis
prime
principal_ideal_domain
ring_invo
roots_of_unity
simple_module
subring
subsemiring
tensor_product
trace
unique_factorization_domain
set_theory
game
domineering
impartial
nim
short
state
winner
cardinal
cardinal_ordinal
cofinality
game
lists
ordinal
ordinal_arithmetic
ordinal_notation
pgame
schroeder_bernstein
surreal
zfc
system
random
basic
tactic
converter
apply_congr
binders
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
rewrite_all
basic
rewrite_search
discovery
explain
frontend
search
types
abel
algebra
alias
apply
apply_fun
auto_cases
binder_matching
cache
cancel_denoms
chain
choose
clear
congr
core
dec_trivial
delta_instance
dependencies
derive_fintype
derive_inhabited
doc_commands
elementwise
elide
equiv_rw
explode
explode_widget
ext
field_simp
fin_cases
find
find_unused
finish
fix_reflect_string
fresh_names
generalize_proofs
generalizes
group
has_variable_names
hint
induction
interactive
interactive_expr
interval_cases
itauto
lean_core_docs
lift
local_cache
localized
mk_iff_of_inductive_prop
noncomm_ring
norm_cast
norm_fin
norm_num
norm_swap
obviously
pi_instances
pretty_cases
protected
push_neg
rcases
reassoc_axiom
rename_var
replacer
reserved_notation
restate_axiom
rewrite
ring
ring2
ring_exp
scc
show_term
simp_command
simp_result
simp_rw
simpa
simps
slice
slim_check
solve_by_elim
split_ifs
squeeze
subtype_instance
suggest
tauto
tfae
tidy
transfer
transform_decl
transport
trunc_cases
unfold_cases
unify_equations
where
with_local_reducibility
wlog
zify
testing
slim_check
functions
gen
sampleable
testable
topology
algebra
nonarchimedean
basic
ordered
proj_Icc
affine
algebra
field
floor_ring
group
group_completion
group_with_zero
infinite_sum
module
monoid
mul_action
multilinear
normed_group
open_subgroup
ordered
polynomial
ring
uniform_group
uniform_ring
category
Profinite
as_limit
default
Top
adjunctions
basic
epi_mono
limits
open_nhds
opens
CompHaus
Compactum
TopCommRing
UniformSpace
continuous_function
algebra
basic
bounded
compact
polynomial
stone_weierstrass
weierstrass
instances
ennreal
nnreal
real
real_vector_space
locally_constant
algebra
basic
metric_space
antilipschitz
baire
basic
cau_seq_filter
closeds
completion
contracting
emetric_space
gluing
gromov_hausdorff
gromov_hausdorff_realized
hausdorff_distance
isometry
kuratowski
lipschitz
metric_separated
pi_Lp
sheaves
sheaf_condition
equalizer_products
opens_le_cover
pairwise_intersections
unique_gluing
forget
limits
local_predicate
presheaf
presheaf_of_functions
sheaf
sheaf_of_functions
sheafify
stalks
uniform_space
absolute_value
abstract_completion
basic
cauchy
compact_separated
compare_reals
complete_separated
completion
pi
separation
uniform_convergence
uniform_embedding
G_delta
bases
basic
compact_open
compacts
connected
constructions
continuous_on
dense_embedding
discrete_quotient
extend_from_subset
homeomorph
list
local_extr
local_homeomorph
maps
omega_complete_partial_order
opens
order
paracompact
path_connected
separation
sequences
shrinking_lemma
stone_cech
subset_properties
tactic
topological_fiber_bundle
unit_interval
urysohns_lemma
vector_bundle