algebra.field.basic - mathlib3 docs

source

theorem add_div {α : Type u_1} [division_semiring α] (a b c : α) :

(a + b) / c = a / c + b / c

source

theorem div_add_div_same {α : Type u_1} [division_semiring α] (a b c : α) :

a / c + b / c = (a + b) / c

source

theorem same_add_div {α : Type u_1} [division_semiring α] {a b : α} (h : b ≠ 0) :

(b + a) / b = 1 + a / b

source

theorem div_add_same {α : Type u_1} [division_semiring α] {a b : α} (h : b ≠ 0) :

(a + b) / b = a / b + 1

source

theorem one_add_div {α : Type u_1} [division_semiring α] {a b : α} (h : b ≠ 0) :

1 + a / b = (b + a) / b

source

theorem div_add_one {α : Type u_1} [division_semiring α] {a b : α} (h : b ≠ 0) :

a / b + 1 = (a + b) / b

source

theorem one_div_mul_add_mul_one_div_eq_one_div_add_one_div {α : Type u_1} [division_semiring α] {a b : α} (ha : a ≠ 0) (hb : b ≠ 0) :

1 / a * (a + b) * (1 / b) = 1 / a + 1 / b

source

theorem add_div_eq_mul_add_div {α : Type u_1} [division_semiring α] {c : α} (a b : α) (hc : c ≠ 0) :

a + b / c = (a * c + b) / c

source

theorem add_div' {α : Type u_1} [division_semiring α] (a b c : α) (hc : c ≠ 0) :

b + a / c = (b * c + a) / c

source

theorem div_add' {α : Type u_1} [division_semiring α] (a b c : α) (hc : c ≠ 0) :

a / c + b = (a + b * c) / c

source

@[protected]

theorem commute.div_add_div {α : Type u_1} [division_semiring α] {a b c d : α} (hbc : commute b c) (hbd : commute b d) (hb : b ≠ 0) (hd : d ≠ 0) :

a / b + c / d = (a * d + b * c) / (b * d)

source

@[protected]

theorem commute.one_div_add_one_div {α : Type u_1} [division_semiring α] {a b : α} (hab : commute a b) (ha : a ≠ 0) (hb : b ≠ 0) :

1 / a + 1 / b = (a + b) / (a * b)

source

@[protected]

theorem commute.inv_add_inv {α : Type u_1} [division_semiring α] {a b : α} (hab : commute a b) (ha : a ≠ 0) (hb : b ≠ 0) :

a⁻¹ + b⁻¹ = (a + b) / (a * b)

source

theorem one_div_neg_one_eq_neg_one {K : Type u_3} [division_monoid K] [has_distrib_neg K] :

1 / -1 = -1

source

theorem one_div_neg_eq_neg_one_div {K : Type u_3} [division_monoid K] [has_distrib_neg K] (a : K) :

1 / -a = -(1 / a)

source

theorem div_neg_eq_neg_div {K : Type u_3} [division_monoid K] [has_distrib_neg K] (a b : K) :

b / -a = -(b / a)

source

theorem neg_div {K : Type u_3} [division_monoid K] [has_distrib_neg K] (a b : K) :

-b / a = -(b / a)

source

theorem neg_div' {K : Type u_3} [division_monoid K] [has_distrib_neg K] (a b : K) :

-(b / a) = -b / a

source

theorem neg_div_neg_eq {K : Type u_3} [division_monoid K] [has_distrib_neg K] (a b : K) :

-a / -b = a / b

source

theorem neg_inv {K : Type u_3} [division_monoid K] [has_distrib_neg K] {a : K} :

-a⁻¹ = (-a)⁻¹

source

theorem div_neg {K : Type u_3} [division_monoid K] [has_distrib_neg K] {b : K} (a : K) :

a / -b = -(a / b)

source

theorem inv_neg {K : Type u_3} [division_monoid K] [has_distrib_neg K] {a : K} :

(-a)⁻¹ = -a⁻¹

source

@[simp]

theorem div_neg_self {K : Type u_3} [division_ring K] {a : K} (h : a ≠ 0) :

a / -a = -1

source

@[simp]

theorem neg_div_self {K : Type u_3} [division_ring K] {a : K} (h : a ≠ 0) :

-a / a = -1

source

theorem div_sub_div_same {K : Type u_3} [division_ring K] (a b c : K) :

a / c - b / c = (a - b) / c

source

theorem same_sub_div {K : Type u_3} [division_ring K] {a b : K} (h : b ≠ 0) :

(b - a) / b = 1 - a / b

source

theorem one_sub_div {K : Type u_3} [division_ring K] {a b : K} (h : b ≠ 0) :

1 - a / b = (b - a) / b

source

theorem div_sub_same {K : Type u_3} [division_ring K] {a b : K} (h : b ≠ 0) :

(a - b) / b = a / b - 1

source

theorem div_sub_one {K : Type u_3} [division_ring K] {a b : K} (h : b ≠ 0) :

a / b - 1 = (a - b) / b

source

theorem sub_div {K : Type u_3} [division_ring K] (a b c : K) :

(a - b) / c = a / c - b / c

source

theorem inv_sub_inv' {K : Type u_3} [division_ring K] {a b : K} (ha : a ≠ 0) (hb : b ≠ 0) :

a⁻¹ - b⁻¹ = a⁻¹ * (b - a) * b⁻¹

See inv_sub_inv for the more convenient version when K is commutative.

source

theorem one_div_mul_sub_mul_one_div_eq_one_div_add_one_div {K : Type u_3} [division_ring K] {a b : K} (ha : a ≠ 0) (hb : b ≠ 0) :

1 / a * (b - a) * (1 / b) = 1 / a - 1 / b

source

@[protected, instance]

def division_ring.is_domain {K : Type u_3} [division_ring K] :

is_domain K

source

@[protected]

theorem commute.div_sub_div {K : Type u_3} [division_ring K] {a b c d : K} (hbc : commute b c) (hbd : commute b d) (hb : b ≠ 0) (hd : d ≠ 0) :

a / b - c / d = (a * d - b * c) / (b * d)

source

@[protected]

theorem commute.inv_sub_inv {K : Type u_3} [division_ring K] {a b : K} (hab : commute a b) (ha : a ≠ 0) (hb : b ≠ 0) :

a⁻¹ - b⁻¹ = (b - a) / (a * b)

source

theorem div_add_div {α : Type u_1} [semifield α] {b d : α} (a c : α) (hb : b ≠ 0) (hd : d ≠ 0) :

a / b + c / d = (a * d + b * c) / (b * d)

source

theorem one_div_add_one_div {α : Type u_1} [semifield α] {a b : α} (ha : a ≠ 0) (hb : b ≠ 0) :

1 / a + 1 / b = (a + b) / (a * b)

source

theorem inv_add_inv {α : Type u_1} [semifield α] {a b : α} (ha : a ≠ 0) (hb : b ≠ 0) :

a⁻¹ + b⁻¹ = (a + b) / (a * b)

source

theorem div_sub_div {K : Type u_3} [field K] (a : K) {b : K} (c : K) {d : K} (hb : b ≠ 0) (hd : d ≠ 0) :

a / b - c / d = (a * d - b * c) / (b * d)

source

theorem inv_sub_inv {K : Type u_3} [field K] {a b : K} (ha : a ≠ 0) (hb : b ≠ 0) :

a⁻¹ - b⁻¹ = (b - a) / (a * b)

source

theorem sub_div' {K : Type u_3} [field K] (a b c : K) (hc : c ≠ 0) :

b - a / c = (b * c - a) / c

source

theorem div_sub' {K : Type u_3} [field K] (a b c : K) (hc : c ≠ 0) :

a / c - b = (a - c * b) / c

source

@[protected, instance]

def field.is_domain {K : Type u_3} [field K] :

is_domain K

source

@[protected]

theorem ring_hom.injective {α : Type u_1} {β : Type u_2} [division_ring α] [semiring β] [nontrivial β] (f : α →+* β) :

function.injective ⇑f

source

noncomputable def division_ring_of_is_unit_or_eq_zero {R : Type u_4} [nontrivial R] [hR : ring R] (h : ∀ (a : R), is_unit a ∨ a = 0) :

division_ring R

Constructs a division_ring structure on a ring consisting only of units and 0.

Equations

division_ring_of_is_unit_or_eq_zero h = {add := ring.add hR, add_assoc := _, zero := group_with_zero.zero (group_with_zero_of_is_unit_or_eq_zero h), zero_add := _, add_zero := _, nsmul := ring.nsmul hR, nsmul_zero' := _, nsmul_succ' := _, neg := ring.neg hR, sub := ring.sub hR, sub_eq_add_neg := _, zsmul := ring.zsmul hR, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := ring.int_cast hR, nat_cast := ring.nat_cast hR, one := group_with_zero.one (group_with_zero_of_is_unit_or_eq_zero h), nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := group_with_zero.mul (group_with_zero_of_is_unit_or_eq_zero h), mul_assoc := _, one_mul := _, mul_one := _, npow := group_with_zero.npow (group_with_zero_of_is_unit_or_eq_zero h), npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, inv := group_with_zero.inv (group_with_zero_of_is_unit_or_eq_zero h), div := group_with_zero.div (group_with_zero_of_is_unit_or_eq_zero h), div_eq_mul_inv := _, zpow := group_with_zero.zpow (group_with_zero_of_is_unit_or_eq_zero h), zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, exists_pair_ne := _, rat_cast := rat.cast_rec (div_inv_monoid.to_has_inv R), mul_inv_cancel := _, inv_zero := _, rat_cast_mk := _, qsmul := qsmul_rec rat.cast_rec (distrib.to_has_mul R), qsmul_eq_mul' := _}

source

@[reducible]

noncomputable def field_of_is_unit_or_eq_zero {R : Type u_4} [nontrivial R] [hR : comm_ring R] (h : ∀ (a : R), is_unit a ∨ a = 0) :

field R

Constructs a field structure on a comm_ring consisting only of units and 0. See note [reducible non-instances].

Equations

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

source

@[protected, reducible]

def function.injective.division_semiring {α : Type u_1} {β : Type u_2} [division_semiring β] [has_zero α] [has_mul α] [has_add α] [has_one α] [has_inv α] [has_div α] [has_smul ℕ α] [has_pow α ℕ] [has_pow α ℤ] [has_nat_cast α] (f : α → β) (hf : function.injective f) (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (x y : α), f (x + y) = f x + f y) (mul : ∀ (x y : α), f (x * y) = f x * f y) (inv : ∀ (x : α), f x⁻¹ = (f x)⁻¹) (div : ∀ (x y : α), f (x / y) = f x / f y) (nsmul : ∀ (x : α) (n : ℕ), f (n • x) = n • f x) (npow : ∀ (x : α) (n : ℕ), f (x ^ n) = f x ^ n) (zpow : ∀ (x : α) (n : ℤ), f (x ^ n) = f x ^ n) (nat_cast : ∀ (n : ℕ), f ↑n = ↑n) :

division_semiring α

Pullback a division_semiring along an injective function.

Equations

function.injective.division_semiring f hf zero one add mul inv div nsmul npow zpow nat_cast = {add := semiring.add (function.injective.semiring f hf zero one add mul nsmul npow nat_cast), add_assoc := _, zero := group_with_zero.zero (function.injective.group_with_zero f hf zero one mul inv div npow zpow), zero_add := _, add_zero := _, nsmul := semiring.nsmul (function.injective.semiring f hf zero one add mul nsmul npow nat_cast), nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := group_with_zero.mul (function.injective.group_with_zero f hf zero one mul inv div npow zpow), left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := group_with_zero.one (function.injective.group_with_zero f hf zero one mul inv div npow zpow), one_mul := _, mul_one := _, nat_cast := semiring.nat_cast (function.injective.semiring f hf zero one add mul nsmul npow nat_cast), nat_cast_zero := _, nat_cast_succ := _, npow := group_with_zero.npow (function.injective.group_with_zero f hf zero one mul inv div npow zpow), npow_zero' := _, npow_succ' := _, inv := group_with_zero.inv (function.injective.group_with_zero f hf zero one mul inv div npow zpow), div := group_with_zero.div (function.injective.group_with_zero f hf zero one mul inv div npow zpow), div_eq_mul_inv := _, zpow := group_with_zero.zpow (function.injective.group_with_zero f hf zero one mul inv div npow zpow), zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, exists_pair_ne := _, inv_zero := _, mul_inv_cancel := _}

source

@[protected, reducible]

def function.injective.division_ring {K : Type u_3} [division_ring K] {K' : Type u_1} [has_zero K'] [has_one K'] [has_add K'] [has_mul K'] [has_neg K'] [has_sub K'] [has_inv K'] [has_div K'] [has_smul ℕ K'] [has_smul ℤ K'] [has_smul ℚ K'] [has_pow K' ℕ] [has_pow K' ℤ] [has_nat_cast K'] [has_int_cast K'] [has_rat_cast K'] (f : K' → K) (hf : function.injective f) (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (x y : K'), f (x + y) = f x + f y) (mul : ∀ (x y : K'), f (x * y) = f x * f y) (neg : ∀ (x : K'), f (-x) = -f x) (sub : ∀ (x y : K'), f (x - y) = f x - f y) (inv : ∀ (x : K'), f x⁻¹ = (f x)⁻¹) (div : ∀ (x y : K'), f (x / y) = f x / f y) (nsmul : ∀ (x : K') (n : ℕ), f (n • x) = n • f x) (zsmul : ∀ (x : K') (n : ℤ), f (n • x) = n • f x) (qsmul : ∀ (x : K') (n : ℚ), f (n • x) = n • f x) (npow : ∀ (x : K') (n : ℕ), f (x ^ n) = f x ^ n) (zpow : ∀ (x : K') (n : ℤ), f (x ^ n) = f x ^ n) (nat_cast : ∀ (n : ℕ), f ↑n = ↑n) (int_cast : ∀ (n : ℤ), f ↑n = ↑n) (rat_cast : ∀ (n : ℚ), f ↑n = ↑n) :

division_ring K'

Pullback a division_ring along an injective function. See note [reducible non-instances].

Equations

function.injective.division_ring f hf zero one add mul neg sub inv div nsmul zsmul qsmul npow zpow nat_cast int_cast rat_cast = {add := ring.add (function.injective.ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast), add_assoc := _, zero := group_with_zero.zero (function.injective.group_with_zero f hf zero one mul inv div npow zpow), zero_add := _, add_zero := _, nsmul := ring.nsmul (function.injective.ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast), nsmul_zero' := _, nsmul_succ' := _, neg := ring.neg (function.injective.ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast), sub := ring.sub (function.injective.ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast), sub_eq_add_neg := _, zsmul := ring.zsmul (function.injective.ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast), zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := ring.int_cast (function.injective.ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast), nat_cast := ring.nat_cast (function.injective.ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast), one := group_with_zero.one (function.injective.group_with_zero f hf zero one mul inv div npow zpow), nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := group_with_zero.mul (function.injective.group_with_zero f hf zero one mul inv div npow zpow), mul_assoc := _, one_mul := _, mul_one := _, npow := group_with_zero.npow (function.injective.group_with_zero f hf zero one mul inv div npow zpow), npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, inv := group_with_zero.inv (function.injective.group_with_zero f hf zero one mul inv div npow zpow), div := group_with_zero.div (function.injective.group_with_zero f hf zero one mul inv div npow zpow), div_eq_mul_inv := _, zpow := group_with_zero.zpow (function.injective.group_with_zero f hf zero one mul inv div npow zpow), zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, exists_pair_ne := _, rat_cast := coe coe_to_lift, mul_inv_cancel := _, inv_zero := _, rat_cast_mk := _, qsmul := has_smul.smul _inst_12, qsmul_eq_mul' := _}

source

@[protected, reducible]

def function.injective.semifield {α : Type u_1} {β : Type u_2} [semifield β] [has_zero α] [has_mul α] [has_add α] [has_one α] [has_inv α] [has_div α] [has_smul ℕ α] [has_pow α ℕ] [has_pow α ℤ] [has_nat_cast α] (f : α → β) (hf : function.injective f) (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (x y : α), f (x + y) = f x + f y) (mul : ∀ (x y : α), f (x * y) = f x * f y) (inv : ∀ (x : α), f x⁻¹ = (f x)⁻¹) (div : ∀ (x y : α), f (x / y) = f x / f y) (nsmul : ∀ (x : α) (n : ℕ), f (n • x) = n • f x) (npow : ∀ (x : α) (n : ℕ), f (x ^ n) = f x ^ n) (zpow : ∀ (x : α) (n : ℤ), f (x ^ n) = f x ^ n) (nat_cast : ∀ (n : ℕ), f ↑n = ↑n) :

semifield α

Pullback a field along an injective function.

Equations

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

source

@[protected, reducible]

def function.injective.field {K : Type u_3} [field K] {K' : Type u_1} [has_zero K'] [has_mul K'] [has_add K'] [has_neg K'] [has_sub K'] [has_one K'] [has_inv K'] [has_div K'] [has_smul ℕ K'] [has_smul ℤ K'] [has_smul ℚ K'] [has_pow K' ℕ] [has_pow K' ℤ] [has_nat_cast K'] [has_int_cast K'] [has_rat_cast K'] (f : K' → K) (hf : function.injective f) (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (x y : K'), f (x + y) = f x + f y) (mul : ∀ (x y : K'), f (x * y) = f x * f y) (neg : ∀ (x : K'), f (-x) = -f x) (sub : ∀ (x y : K'), f (x - y) = f x - f y) (inv : ∀ (x : K'), f x⁻¹ = (f x)⁻¹) (div : ∀ (x y : K'), f (x / y) = f x / f y) (nsmul : ∀ (x : K') (n : ℕ), f (n • x) = n • f x) (zsmul : ∀ (x : K') (n : ℤ), f (n • x) = n • f x) (qsmul : ∀ (x : K') (n : ℚ), f (n • x) = n • f x) (npow : ∀ (x : K') (n : ℕ), f (x ^ n) = f x ^ n) (zpow : ∀ (x : K') (n : ℤ), f (x ^ n) = f x ^ n) (nat_cast : ∀ (n : ℕ), f ↑n = ↑n) (int_cast : ∀ (n : ℤ), f ↑n = ↑n) (rat_cast : ∀ (n : ℚ), f ↑n = ↑n) :

field K'

Pullback a field along an injective function. See note [reducible non-instances].

Equations