mathlib documentation

Equations

• punit.comm_group = {mul := λ (_x _x : punit), punit.star, mul_assoc := punit.comm_group._proof_1, one := punit.star, one_mul := punit.comm_group._proof_2, mul_one := punit.comm_group._proof_3, inv := λ (_x : punit), punit.star, mul_left_inv := punit.comm_group._proof_4, mul_comm := punit.comm_group._proof_5}

Equations

• punit.comm_ring = {add := add_comm_group.add punit.add_comm_group, add_assoc := _, zero := add_comm_group.zero punit.add_comm_group, zero_add := _, add_zero := _, neg := add_comm_group.neg punit.add_comm_group, add_left_neg := _, add_comm := _, mul := comm_group.mul punit.comm_group, mul_assoc := _, one := comm_group.one punit.comm_group, one_mul := _, mul_one := _, left_distrib := punit.comm_ring._proof_1, right_distrib := punit.comm_ring._proof_2, mul_comm := _}

Equations

• punit.complete_boolean_algebra = {sup := λ (_x _x : punit), punit.star, le := λ (_x _x : punit), true, lt := λ (_x _x : punit), false, le_refl := punit.complete_boolean_algebra._proof_1, le_trans := punit.complete_boolean_algebra._proof_2, lt_iff_le_not_le := punit.complete_boolean_algebra._proof_3, le_antisymm := punit.complete_boolean_algebra._proof_4, le_sup_left := punit.complete_boolean_algebra._proof_5, le_sup_right := punit.complete_boolean_algebra._proof_6, sup_le := punit.complete_boolean_algebra._proof_7, inf := λ (_x _x : punit), punit.star, inf_le_left := punit.complete_boolean_algebra._proof_8, inf_le_right := punit.complete_boolean_algebra._proof_9, le_inf := punit.complete_boolean_algebra._proof_10, le_sup_inf := punit.complete_boolean_algebra._proof_11, top := punit.star, le_top := punit.complete_boolean_algebra._proof_12, bot := punit.star, bot_le := punit.complete_boolean_algebra._proof_13, compl := λ (_x : punit), punit.star, sdiff := λ (_x _x : punit), punit.star, inf_compl_le_bot := punit.complete_boolean_algebra._proof_14, top_le_sup_compl := punit.complete_boolean_algebra._proof_15, sdiff_eq := punit.complete_boolean_algebra._proof_16, Sup := λ (_x : set punit), punit.star, Inf := λ (_x : set punit), punit.star, le_Sup := punit.complete_boolean_algebra._proof_17, Sup_le := punit.complete_boolean_algebra._proof_18, Inf_le := punit.complete_boolean_algebra._proof_19, le_Inf := punit.complete_boolean_algebra._proof_20, infi_sup_le_sup_Inf := punit.complete_boolean_algebra._proof_21, inf_Sup_le_supr_inf := punit.complete_boolean_algebra._proof_22}

Equations

• punit.canonically_ordered_add_monoid = {add := comm_ring.add punit.comm_ring, add_assoc := _, zero := comm_ring.zero punit.comm_ring, zero_add := _, add_zero := _, add_comm := _, le := complete_boolean_algebra.le punit.complete_boolean_algebra, lt := complete_boolean_algebra.lt punit.complete_boolean_algebra, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := punit.canonically_ordered_add_monoid._proof_1, lt_of_add_lt_add_left := punit.canonically_ordered_add_monoid._proof_2, bot := complete_boolean_algebra.bot punit.complete_boolean_algebra, bot_le := _, le_iff_exists_add := punit.canonically_ordered_add_monoid._proof_3}

Equations

• punit.decidable_linear_ordered_cancel_add_comm_monoid = {add := canonically_ordered_add_monoid.add punit.canonically_ordered_add_monoid, add_assoc := _, zero := canonically_ordered_add_monoid.zero punit.canonically_ordered_add_monoid, zero_add := _, add_zero := _, add_comm := _, add_left_cancel := punit.decidable_linear_ordered_cancel_add_comm_monoid._proof_1, add_right_cancel := punit.decidable_linear_ordered_cancel_add_comm_monoid._proof_2, le := canonically_ordered_add_monoid.le punit.canonically_ordered_add_monoid, lt := canonically_ordered_add_monoid.lt punit.canonically_ordered_add_monoid, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, le_of_add_le_add_left := punit.decidable_linear_ordered_cancel_add_comm_monoid._proof_3, le_total := punit.decidable_linear_ordered_cancel_add_comm_monoid._proof_4, decidable_le := λ (_x _x : punit), decidable.true, decidable_eq := punit.decidable_eq, decidable_lt := λ (_x _x : punit), decidable.false}

Equations

• punit.semimodule R = semimodule.of_core {to_has_scalar := {smul := λ (_x : R) (_x : punit), punit.star}, smul_add := _, add_smul := _, mul_smul := _, one_smul := _}