Instances on punit #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file collects facts about algebraic structures on the one-element type, e.g. that it is a commutative ring.
@[protected, instance]
Equations
- punit.add_comm_group = {add := λ (_x _x : punit), punit.star, add_assoc := punit.add_comm_group._proof_1, zero := punit.star, zero_add := punit.add_comm_group._proof_2, add_zero := punit.add_comm_group._proof_3, nsmul := λ (_x : ℕ) (_x : punit), punit.star, nsmul_zero' := punit.add_comm_group._proof_4, nsmul_succ' := punit.add_comm_group._proof_5, neg := λ (_x : punit), punit.star, sub := λ (_x _x : punit), punit.star, sub_eq_add_neg := punit.add_comm_group._proof_6, zsmul := λ (_x : ℤ) (_x : punit), punit.star, zsmul_zero' := punit.add_comm_group._proof_7, zsmul_succ' := punit.add_comm_group._proof_8, zsmul_neg' := punit.add_comm_group._proof_9, add_left_neg := punit.add_comm_group._proof_10, add_comm := punit.add_comm_group._proof_11}
@[protected, instance]
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, npow := λ (_x : ℕ) (_x : punit), punit.star, npow_zero' := punit.comm_group._proof_4, npow_succ' := punit.comm_group._proof_5, inv := λ (_x : punit), punit.star, div := λ (_x _x : punit), punit.star, div_eq_mul_inv := punit.comm_group._proof_6, zpow := λ (_x : ℤ) (_x : punit), punit.star, zpow_zero' := punit.comm_group._proof_7, zpow_succ' := punit.comm_group._proof_8, zpow_neg' := punit.comm_group._proof_9, mul_left_inv := punit.comm_group._proof_10, mul_comm := punit.comm_group._proof_11}
@[protected, instance]
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 := _, nsmul := add_comm_group.nsmul punit.add_comm_group, nsmul_zero' := _, nsmul_succ' := _, neg := add_comm_group.neg punit.add_comm_group, sub := add_comm_group.sub punit.add_comm_group, sub_eq_add_neg := _, zsmul := add_comm_group.zsmul punit.add_comm_group, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := ring.int_cast._default (λ (_x : ℕ), punit.star) add_comm_group.add add_comm_group.add_assoc add_comm_group.zero add_comm_group.zero_add add_comm_group.add_zero add_comm_group.nsmul add_comm_group.nsmul_zero' add_comm_group.nsmul_succ' comm_group.one rfl punit.comm_ring._proof_1 add_comm_group.neg add_comm_group.sub add_comm_group.sub_eq_add_neg add_comm_group.zsmul add_comm_group.zsmul_zero' add_comm_group.zsmul_succ' add_comm_group.zsmul_neg' add_comm_group.add_left_neg, nat_cast := λ (_x : ℕ), punit.star, one := comm_group.one punit.comm_group, nat_cast_zero := _, nat_cast_succ := punit.comm_ring._proof_2, int_cast_of_nat := punit.comm_ring._proof_3, int_cast_neg_succ_of_nat := punit.comm_ring._proof_4, mul := comm_group.mul punit.comm_group, mul_assoc := _, one_mul := _, mul_one := _, npow := comm_group.npow punit.comm_group, npow_zero' := _, npow_succ' := _, left_distrib := punit.comm_ring._proof_5, right_distrib := punit.comm_ring._proof_6, mul_comm := _}
@[protected, instance]
Equations
- punit.cancel_comm_monoid_with_zero = {mul := comm_ring.mul punit.comm_ring, mul_assoc := _, one := comm_ring.one punit.comm_ring, one_mul := _, mul_one := _, npow := comm_ring.npow punit.comm_ring, npow_zero' := _, npow_succ' := _, mul_comm := _, zero := comm_ring.zero punit.comm_ring, zero_mul := punit.cancel_comm_monoid_with_zero._proof_1, mul_zero := punit.cancel_comm_monoid_with_zero._proof_2, mul_left_cancel_of_ne_zero := punit.cancel_comm_monoid_with_zero._proof_3}
@[protected, instance]
Equations
- punit.normalized_gcd_monoid = {to_normalization_monoid := {norm_unit := λ (x : punit), 1, norm_unit_zero := punit.normalized_gcd_monoid._proof_1, norm_unit_mul := punit.normalized_gcd_monoid._proof_2, norm_unit_coe_units := punit.normalized_gcd_monoid._proof_3}, to_gcd_monoid := {gcd := λ (_x _x : punit), punit.star, lcm := λ (_x _x : punit), punit.star, gcd_dvd_left := punit.normalized_gcd_monoid._proof_4, gcd_dvd_right := punit.normalized_gcd_monoid._proof_5, dvd_gcd := punit.normalized_gcd_monoid._proof_6, gcd_mul_lcm := punit.normalized_gcd_monoid._proof_7, lcm_zero_left := punit.normalized_gcd_monoid._proof_8, lcm_zero_right := punit.normalized_gcd_monoid._proof_9}, normalize_gcd := punit.normalized_gcd_monoid._proof_10, normalize_lcm := punit.normalized_gcd_monoid._proof_11}
@[protected, instance]
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 := _, nsmul := comm_ring.nsmul punit.comm_ring, nsmul_zero' := _, nsmul_succ' := _, 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, bot := complete_boolean_algebra.bot punit.complete_boolean_algebra, bot_le := _, exists_add_of_le := punit.canonically_ordered_add_monoid._proof_2, le_self_add := punit.canonically_ordered_add_monoid._proof_3}
@[protected, instance]
Equations
- punit.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 := _, nsmul := canonically_ordered_add_monoid.nsmul punit.canonically_ordered_add_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, 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.linear_ordered_cancel_add_comm_monoid._proof_1, le_total := _, decidable_le := linear_order.decidable_le punit.linear_order, decidable_eq := linear_order.decidable_eq punit.linear_order, decidable_lt := linear_order.decidable_lt punit.linear_order, max := linear_order.max punit.linear_order, max_def := _, min := linear_order.min punit.linear_order, min_def := _}
@[protected, instance]
Equations
- punit.linear_ordered_add_comm_monoid_with_top = {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 := _, le_total := _, decidable_le := linear_ordered_cancel_add_comm_monoid.decidable_le punit.linear_ordered_cancel_add_comm_monoid, decidable_eq := linear_ordered_cancel_add_comm_monoid.decidable_eq punit.linear_ordered_cancel_add_comm_monoid, decidable_lt := linear_ordered_cancel_add_comm_monoid.decidable_lt punit.linear_ordered_cancel_add_comm_monoid, max := linear_ordered_cancel_add_comm_monoid.max punit.linear_ordered_cancel_add_comm_monoid, max_def := _, min := linear_ordered_cancel_add_comm_monoid.min punit.linear_ordered_cancel_add_comm_monoid, min_def := _, add := linear_ordered_cancel_add_comm_monoid.add punit.linear_ordered_cancel_add_comm_monoid, add_assoc := _, zero := linear_ordered_cancel_add_comm_monoid.zero punit.linear_ordered_cancel_add_comm_monoid, zero_add := _, add_zero := _, nsmul := linear_ordered_cancel_add_comm_monoid.nsmul punit.linear_ordered_cancel_add_comm_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, add_le_add_left := _, top := complete_boolean_algebra.top punit.complete_boolean_algebra, le_top := _, top_add' := punit.linear_ordered_add_comm_monoid_with_top._proof_1}
@[protected, instance]
Equations
- punit.has_smul = {smul := λ (_x : R) (_x : punit), punit.star}
@[protected, instance]
Equations
- punit.has_vadd = {vadd := λ (_x : R) (_x : punit), punit.star}
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
Equations
- punit.smul_with_zero = {to_smul_zero_class := {to_has_smul := {smul := has_smul.smul punit.has_smul}, smul_zero := _}, zero_smul := _}
@[protected, instance]
Equations
- punit.mul_action = {to_has_smul := {smul := has_smul.smul punit.has_smul}, one_smul := _, mul_smul := _}
@[protected, instance]
Equations
- punit.distrib_mul_action = {to_mul_action := {to_has_smul := mul_action.to_has_smul punit.mul_action, one_smul := _, mul_smul := _}, smul_zero := _, smul_add := _}
@[protected, instance]
Equations
- punit.mul_distrib_mul_action = {to_mul_action := {to_has_smul := mul_action.to_has_smul punit.mul_action, one_smul := _, mul_smul := _}, smul_mul := _, smul_one := _}
@[protected, instance]
Equations
- punit.mul_semiring_action = {to_distrib_mul_action := {to_mul_action := distrib_mul_action.to_mul_action punit.distrib_mul_action, smul_zero := _, smul_add := _}, smul_one := _, smul_mul := _}
@[protected, instance]
Equations
- punit.mul_action_with_zero = {to_mul_action := {to_has_smul := mul_action.to_has_smul punit.mul_action, one_smul := _, mul_smul := _}, smul_zero := _, zero_smul := _}
@[protected, instance]
Equations
- punit.module = {to_distrib_mul_action := {to_mul_action := distrib_mul_action.to_mul_action punit.distrib_mul_action, smul_zero := _, smul_add := _}, add_smul := _, zero_smul := _}