Theory of proveit

This is the top-level theory for general "textbook" mathematics.

import proveit
%theory # toggles between interactive and static modes

Local content of this theory

common expressions	axioms	theorems	demonstrations

Sub-theories

core_expr_types	theories pertaining to some of the core exression types
logic	basic logic concepts: boolean arithmetic, equality, and set theory.
numbers	basic number concepts and operations for whole numbers, real numbers, and complex numbers.
trigonometry	theory of lengths and angles of triangles as well as their connection to complex numbers
abstract_algebra	abstract algebra concepts: groups, rings, and fields
linear_algebra	basic concepts in linear algebra: matrix product, etc
statistics	basic statistical concepts
physics	basic physics-related concepts, including quantum topics

All axioms contained within this theory

This theory contains no axioms directly.

proveit.core_expr_types

proveit.core_expr_types.operations.operands_substitution

proveit.core_expr_types.conditionals.true_condition_reduction

proveit.core_expr_types.conditionals.condition_replacement

proveit.core_expr_types.conditionals.condition__as__condition_eq_true

proveit.core_expr_types.conditionals.conditional_substitution

proveit.core_expr_types.conditionals.true_case_reduction

proveit.core_expr_types.lambda_maps.lambda_substitution

proveit.core_expr_types.lambda_maps.unary_composition

proveit.core_expr_types.lambda_maps.binary_composition

proveit.core_expr_types.lambda_maps.multi_composition_def

proveit.core_expr_types.tuples.tuple_len_0

proveit.core_expr_types.tuples.tuple_len_incr

proveit.core_expr_types.tuples.tuple_eq_def

proveit.core_expr_types.tuples.tuple_neq_with_diff_len

proveit.core_expr_types.tuples.empty_range_def

proveit.core_expr_types.tuples.range_extension_def

proveit.core_expr_types.expr_arrays.array_eq_def

proveit.core_expr_types.expr_arrays.varray_eq_def

proveit.core_expr_types.expr_arrays.array_neq_with_diff_len

proveit.core_expr_types.expr_arrays.varray_neq_with_diff_len

proveit.logic

proveit.logic.booleans.true_axiom

proveit.logic.booleans.bools_def

proveit.logic.booleans.false_not_true

proveit.logic.booleans.eq_true_intro

proveit.logic.booleans.eq_true_elim

proveit.logic.booleans.implication.implies_t_f

proveit.logic.booleans.implication.affirmation_via_contradiction

proveit.logic.booleans.implication.denial_via_contradiction

proveit.logic.booleans.implication.iff_def

proveit.logic.booleans.negation.not_t

proveit.logic.booleans.negation.not_f

proveit.logic.booleans.negation.negation_elim

proveit.logic.booleans.negation.operand_is_bool

proveit.logic.booleans.conjunction.and_t_t

proveit.logic.booleans.conjunction.and_t_f

proveit.logic.booleans.conjunction.and_f_t

proveit.logic.booleans.conjunction.and_f_f

proveit.logic.booleans.conjunction.left_in_bool

proveit.logic.booleans.conjunction.right_in_bool

proveit.logic.booleans.conjunction.empty_conjunction

proveit.logic.booleans.conjunction.multi_conjunction_def

proveit.logic.booleans.disjunction.or_t_t

proveit.logic.booleans.disjunction.or_t_f

proveit.logic.booleans.disjunction.or_f_t

proveit.logic.booleans.disjunction.or_f_f

proveit.logic.booleans.disjunction.left_in_bool

proveit.logic.booleans.disjunction.right_in_bool

proveit.logic.booleans.disjunction.empty_disjunction

proveit.logic.booleans.disjunction.multi_disjunction_def

proveit.logic.booleans.quantification.universality.forall_in_bool

proveit.logic.booleans.quantification.existence.exists_def

proveit.logic.booleans.quantification.existence.not_exists_def

proveit.logic.equality.equality_in_bool

proveit.logic.equality.equals_transitivity

proveit.logic.equality.equals_reflexivity

proveit.logic.equality.equals_symmetry

proveit.logic.equality.not_equals_def

proveit.logic.equality.substitution

proveit.logic.sets.membership.not_in_set_def

proveit.logic.sets.equivalence.set_equiv_def

proveit.logic.sets.equivalence.set_not_equiv_def

proveit.logic.sets.enumeration.enum_set_def

proveit.logic.sets.enumeration.empty_set_def

proveit.logic.sets.inclusion.subset_eq_def

proveit.logic.sets.inclusion.not_subset_eq_def

proveit.logic.sets.inclusion.proper_subset_def

proveit.logic.sets.inclusion.not_proper_subset_def

proveit.logic.sets.unification.union_def

proveit.logic.sets.unification.union_all_def

proveit.logic.sets.intersection.intersection_def

proveit.logic.sets.intersection.intersect_all_def

proveit.logic.sets.subtraction.difference_def

proveit.logic.sets.comprehension.comprehension_def

proveit.logic.sets.power_set.power_set_def

proveit.logic.sets.cartesian_products.cart_prod_def

proveit.logic.sets.cartesian_products.cart_exp_def

proveit.logic.sets.disjointness.vacuously_disjoint

proveit.logic.sets.disjointness.disjoint_pair_def

proveit.logic.sets.disjointness.disjoint_induction

proveit.logic.sets.disjointness.distinct_def

proveit.logic.sets.cardinality.empty_card

proveit.logic.sets.cardinality.card_induction

proveit.logic.sets.functions.functions_def

proveit.logic.sets.functions.images.set_image_def

proveit.logic.sets.functions.injections.injective_def

proveit.logic.sets.functions.surjections.surjective_def

proveit.logic.sets.functions.bijections.bijective_def

proveit.logic.classes.membership.not_in_class_def

proveit.numbers

proveit.numbers.number_sets.natural_numbers.zero_in_nats

proveit.numbers.number_sets.natural_numbers.successor_in_nats

proveit.numbers.number_sets.natural_numbers.successor_is_injective

proveit.numbers.number_sets.natural_numbers.zero_not_successor

proveit.numbers.number_sets.natural_numbers.induction

proveit.numbers.number_sets.natural_numbers.boolean_natural_membership

proveit.numbers.number_sets.natural_numbers.natural_pos_def

proveit.numbers.number_sets.integers.integers_def

proveit.numbers.number_sets.integers.integer_interval_is_subset_of_integers

proveit.numbers.number_sets.integers.integer_interval_element_bounds

proveit.numbers.number_sets.rational_numbers.rationals_def

proveit.numbers.number_sets.rational_numbers.rationals_pos_def

proveit.numbers.number_sets.rational_numbers.rationals_neg_def

proveit.numbers.number_sets.rational_numbers.rationals_non_neg_def

proveit.numbers.number_sets.real_numbers.real_pos_def

proveit.numbers.number_sets.real_numbers.in_IntervalOO_def

proveit.numbers.number_sets.real_numbers.in_IntervalOC_def

proveit.numbers.number_sets.real_numbers.in_IntervalCO_def

proveit.numbers.number_sets.real_numbers.in_IntervalCC_def

proveit.numbers.number_sets.complex_numbers.imaginary_number_def

proveit.numbers.number_sets.complex_numbers.complex_numbers_def

proveit.numbers.number_sets.complex_numbers.conjugate_def

proveit.numbers.rounding.ceil_is_an_int

proveit.numbers.rounding.ceil_of_x_greater_eq_x

proveit.numbers.rounding.ceil_of_x_less_eq

proveit.numbers.rounding.floor_is_an_int

proveit.numbers.rounding.floor_of_x_less_eq_x

proveit.numbers.rounding.floor_of_x_greater_eq

proveit.numbers.rounding.round_is_an_int

proveit.numbers.rounding.round_is_closest_int

proveit.numbers.rounding.round_up

proveit.numbers.absolute_value.abs_val_def_sqrt

proveit.numbers.numerals.binaries.single_bit_reduction

proveit.numbers.numerals.decimals.one_def

proveit.numbers.numerals.decimals.two_def

proveit.numbers.numerals.decimals.three_def

proveit.numbers.numerals.decimals.four_def

proveit.numbers.numerals.decimals.five_def

proveit.numbers.numerals.decimals.six_def

proveit.numbers.numerals.decimals.seven_def

proveit.numbers.numerals.decimals.eight_def

proveit.numbers.numerals.decimals.nine_def

proveit.numbers.numerals.decimals.N_leq_9_def

proveit.numbers.numerals.decimals.single_digit_reduction

proveit.numbers.addition.nat_plus_zero

proveit.numbers.addition.nat_plus_successor

proveit.numbers.addition.empty_addition

proveit.numbers.addition.multi_addition_def

proveit.numbers.negation.negation_is_injunctive

proveit.numbers.negation.neg_def_add_inv

proveit.numbers.ordering.less_eq_def

proveit.numbers.ordering.transitivity_less_less

proveit.numbers.ordering.max_def_unary

proveit.numbers.ordering.min_def_unary

proveit.numbers.ordering.max_def_bin

proveit.numbers.ordering.min_def_bin

proveit.numbers.ordering.max_def_multi

proveit.numbers.ordering.min_def_multi

proveit.numbers.multiplication.mult_def

proveit.numbers.multiplication.empty_mult

proveit.numbers.multiplication.multi_mult_def

proveit.numbers.divisibility.divides_def

proveit.numbers.modular.mod_greater_eq_zero

proveit.numbers.modular.mod_less_modulus

proveit.numbers.modular.mod_is_remainder

proveit.numbers.modular.mod_abs_def

proveit.numbers.exponentiation.nat_exp_def

proveit.numbers.summation.sum_single

proveit.numbers.summation.sum_split_last

proveit.numbers.summation.breakup_sum

proveit.numbers.functions.kron_delta_def

proveit.trigonometry

This sub-theory contains no axioms.

proveit.abstract_algebra

This sub-theory contains no axioms.

proveit.linear_algebra

proveit.linear_algebra.linear_map_unary_addition

proveit.linear_algebra.linear_map_binary_addition

proveit.linear_algebra.linear_map_multi_addition

proveit.linear_algebra.tensor_exp_one

proveit.linear_algebra.addition.scalar_add_extends_number_add

proveit.linear_algebra.addition.scalar_sum_extends_number_sum

proveit.linear_algebra.addition.vec_sum_single

proveit.linear_algebra.addition.vec_sum_split_last

proveit.linear_algebra.scalar_multiplication.scalar_mult_extends_number_mult

proveit.linear_algebra.inner_products.inner_prod_space_def

proveit.linear_algebra.inner_products.hilbert_space_def

proveit.linear_algebra.inner_products.norm_def

proveit.linear_algebra.inner_products.ortho_norm_bases_def

proveit.linear_algebra.inner_products.ortho_proj_def

proveit.linear_algebra.vector_sets.span_def

proveit.linear_algebra.vector_sets.spanning_set_def

proveit.linear_algebra.vector_sets.lindep_set_def

proveit.linear_algebra.vector_sets.bases_def

proveit.linear_algebra.vector_sets.dim_def

proveit.linear_algebra.linear_maps.lin_map_def

proveit.linear_algebra.linear_maps.vec_add_lin_map

proveit.linear_algebra.linear_maps.scalar_mult_lin_map

proveit.linear_algebra.linear_maps.identity_def

proveit.linear_algebra.linear_maps.commutator_def

proveit.linear_algebra.linear_maps.anti_commutator_def

proveit.linear_algebra.tensors.unary_tensor_prod_def

proveit.linear_algebra.tensors.tensor_prod_in_vec_space_only_if_valid

proveit.linear_algebra.tensors.multi_tensor_prod_def

proveit.statistics

proveit.statistics.samples_space_def

proveit.statistics.event_prob_def

proveit.statistics.prob_of_all_def

proveit.physics

proveit.physics.quantum.hadamard_on_zero

proveit.physics.quantum.substitution

proveit.physics.quantum.algebra.ket_zero_def

proveit.physics.quantum.algebra.ket_one_def

proveit.physics.quantum.algebra.ket_plus_def

proveit.physics.quantum.algebra.ket_minus_def

proveit.physics.quantum.algebra.num_ket_def

proveit.physics.quantum.algebra.bra_def

proveit.physics.quantum.algebra.qmult_of_ket

proveit.physics.quantum.algebra.qmult_of_matrix

proveit.physics.quantum.algebra.qmult_of_linmap

proveit.physics.quantum.algebra.qmult_op_ket

proveit.physics.quantum.algebra.qmult_op_op

proveit.physics.quantum.algebra.qmult_ket_ket

proveit.physics.quantum.algebra.qmult_ket_bra

proveit.physics.quantum.algebra.qmult_complex_complex

proveit.physics.quantum.algebra.qmult_complex_left

proveit.physics.quantum.algebra.qmult_complex_right

proveit.physics.quantum.algebra.qmult_in_codomain_only_if_valid

proveit.physics.quantum.algebra.multi_qmult_def

proveit.physics.quantum.circuits.qcircuit_eq_def

proveit.physics.quantum.circuits.qcircuit_input_eq_def

proveit.physics.quantum.circuits.qcircuit_output_eq_def

proveit.physics.quantum.circuits.qcircuit_input_part_eq_def

proveit.physics.quantum.circuits.qcircuit_output_part_eq_def

proveit.physics.quantum.QPE.QPE1_def

proveit.physics.quantum.QPE.QPE_def

proveit.physics.quantum.QPE._t_in_natural_pos

proveit.physics.quantum.QPE._s_in_nat_pos

proveit.physics.quantum.QPE._unitary_U

proveit.physics.quantum.QPE._u_ket_register

proveit.physics.quantum.QPE._normalized_ket_u

proveit.physics.quantum.QPE._phase_in_interval

proveit.physics.quantum.QPE._eigen_uu

proveit.physics.quantum.QPE._mod_add_def

proveit.physics.quantum.QPE._psi_t_def

proveit.physics.quantum.QPE._Psi_def

proveit.physics.quantum.QPE._sample_space_def

proveit.physics.quantum.QPE._alpha_m_def

proveit.physics.quantum.QPE._best_floor_def

proveit.physics.quantum.QPE._best_round_def

proveit.physics.quantum.QPE._delta_b_def

proveit.physics.quantum.QPE._success_def

proveit.physics.quantum.QPE._fail_def

proveit.physics.quantum.QPE._n_in_natural_pos

proveit.physics.quantum.QPE._n_ge_two

proveit.physics.quantum.QPE._eps_in_interval

proveit.physics.quantum.QPE._t_req