mathlib3 documentation

algebra.field.ulift

Field instances for `ulift` #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines instances for field, semifield and related structures on ulift types.

(Recall ulift α is just a "copy" of a type α in a higher universe.)

@[protected, instance]

def ulift.has_rat_cast {α : Type u} [has_rat_cast α] :

has_rat_cast (ulift α)

Equations

ulift.has_rat_cast = {rat_cast := λ (a : ℚ), {down := ↑a}}

@[simp, norm_cast]

theorem ulift.up_rat_cast {α : Type u} [has_rat_cast α] (q : ℚ) :

{down := ↑q} = ↑q

@[simp, norm_cast]

theorem ulift.down_rat_cast {α : Type u} [has_rat_cast α] (q : ℚ) :

↑q.down = ↑q

@[protected, instance]

def ulift.division_semiring {α : Type u} [division_semiring α] :

division_semiring (ulift α)

Equations

ulift.division_semiring = function.injective.division_semiring ulift.down ulift.down_injective ulift.division_semiring._proof_1 ulift.division_semiring._proof_2 ulift.division_semiring._proof_3 ulift.division_semiring._proof_4 ulift.division_semiring._proof_5 ulift.division_semiring._proof_6 ulift.division_semiring._proof_7 ulift.division_semiring._proof_8 ulift.division_semiring._proof_9 ulift.division_semiring._proof_10

@[protected, instance]

def ulift.semifield {α : Type u} [semifield α] :

semifield (ulift α)

Equations

ulift.semifield = {add := division_semiring.add ulift.division_semiring, add_assoc := _, zero := division_semiring.zero ulift.division_semiring, zero_add := _, add_zero := _, nsmul := division_semiring.nsmul ulift.division_semiring, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := division_semiring.mul ulift.division_semiring, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := division_semiring.one ulift.division_semiring, one_mul := _, mul_one := _, nat_cast := division_semiring.nat_cast ulift.division_semiring, nat_cast_zero := _, nat_cast_succ := _, npow := division_semiring.npow ulift.division_semiring, npow_zero' := _, npow_succ' := _, mul_comm := _, inv := division_semiring.inv ulift.division_semiring, div := division_semiring.div ulift.division_semiring, div_eq_mul_inv := _, zpow := division_semiring.zpow ulift.division_semiring, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, exists_pair_ne := _, inv_zero := _, mul_inv_cancel := _}

@[protected, instance]

def ulift.division_ring {α : Type u} [division_ring α] :

division_ring (ulift α)

Equations

ulift.division_ring = {add := division_semiring.add ulift.division_semiring, add_assoc := _, zero := division_semiring.zero ulift.division_semiring, zero_add := _, add_zero := _, nsmul := division_semiring.nsmul ulift.division_semiring, nsmul_zero' := _, nsmul_succ' := _, neg := add_group.neg ulift.add_group, sub := add_group.sub ulift.add_group, sub_eq_add_neg := _, zsmul := add_group.zsmul ulift.add_group, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := ring.int_cast._default division_semiring.nat_cast division_semiring.add ulift.division_ring._proof_12 division_semiring.zero ulift.division_ring._proof_13 ulift.division_ring._proof_14 division_semiring.nsmul ulift.division_ring._proof_15 ulift.division_ring._proof_16 division_semiring.one ulift.division_ring._proof_17 ulift.division_ring._proof_18 add_group.neg add_group.sub ulift.division_ring._proof_19 add_group.zsmul ulift.division_ring._proof_20 ulift.division_ring._proof_21 ulift.division_ring._proof_22 ulift.division_ring._proof_23, nat_cast := division_semiring.nat_cast ulift.division_semiring, one := division_semiring.one ulift.division_semiring, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := division_semiring.mul ulift.division_semiring, mul_assoc := _, one_mul := _, mul_one := _, npow := division_semiring.npow ulift.division_semiring, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, inv := division_semiring.inv ulift.division_semiring, div := division_semiring.div ulift.division_semiring, div_eq_mul_inv := _, zpow := division_semiring.zpow ulift.division_semiring, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, exists_pair_ne := _, rat_cast := rat.cast_rec (div_inv_monoid.to_has_inv (ulift α)), mul_inv_cancel := _, inv_zero := _, rat_cast_mk := _, qsmul := qsmul_rec rat.cast_rec (distrib.to_has_mul (ulift α)), qsmul_eq_mul' := _}

@[protected, instance]

def ulift.field {α : Type u} [field α] :

field (ulift α)

Equations

ulift.field = {add := semifield.add ulift.semifield, add_assoc := _, zero := semifield.zero ulift.semifield, zero_add := _, add_zero := _, nsmul := semifield.nsmul ulift.semifield, nsmul_zero' := _, nsmul_succ' := _, neg := division_ring.neg ulift.division_ring, sub := division_ring.sub ulift.division_ring, sub_eq_add_neg := _, zsmul := division_ring.zsmul ulift.division_ring, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := division_ring.int_cast ulift.division_ring, nat_cast := semifield.nat_cast ulift.semifield, one := semifield.one ulift.semifield, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := semifield.mul ulift.semifield, mul_assoc := _, one_mul := _, mul_one := _, npow := semifield.npow ulift.semifield, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, mul_comm := _, inv := semifield.inv ulift.semifield, div := semifield.div ulift.semifield, div_eq_mul_inv := _, zpow := semifield.zpow ulift.semifield, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, exists_pair_ne := _, rat_cast := division_ring.rat_cast ulift.division_ring, mul_inv_cancel := _, inv_zero := _, rat_cast_mk := _, qsmul := division_ring.qsmul ulift.division_ring, qsmul_eq_mul' := _}