Field structure on the multiplicative/additive opposite

instance AddOpposite.ratCast (α : Type u_1) [RatCast α] : RatCast αᵃᵒᵖ

Equations

• AddOpposite.ratCast α = { ratCast := fun (n : ℚ) => AddOpposite.op ↑n }

instance MulOpposite.ratCast (α : Type u_1) [RatCast α] : RatCast αᵐᵒᵖ

Equations

• MulOpposite.ratCast α = { ratCast := fun (n : ℚ) => MulOpposite.op ↑n }

@[simp]

theorem AddOpposite.op_ratCast {α : Type u_1} [RatCast α] (q : ℚ) : AddOpposite.op ↑q = ↑q

@[simp]

theorem MulOpposite.op_ratCast {α : Type u_1} [RatCast α] (q : ℚ) : MulOpposite.op ↑q = ↑q

@[simp]

theorem AddOpposite.unop_ratCast {α : Type u_1} [RatCast α] (q : ℚ) : AddOpposite.unop ↑q = ↑q

@[simp]

theorem MulOpposite.unop_ratCast {α : Type u_1} [RatCast α] (q : ℚ) : MulOpposite.unop ↑q = ↑q

instance MulOpposite.instDivisionSemiring (α : Type u_1) [DivisionSemiring α] : DivisionSemiring αᵐᵒᵖ

Equations

• MulOpposite.instDivisionSemiring α = let __src := MulOpposite.instGroupWithZero α; let __src_1 := MulOpposite.instSemiring α; DivisionSemiring.mk ⋯ GroupWithZero.zpow ⋯ ⋯ ⋯ ⋯ ⋯

instance MulOpposite.instDivisionRing (α : Type u_1) [DivisionRing α] : DivisionRing αᵐᵒᵖ

Equations

• One or more equations did not get rendered due to their size.

instance MulOpposite.instSemifield (α : Type u_1) [Semifield α] : Semifield αᵐᵒᵖ

Equations

• MulOpposite.instSemifield α = let __src := MulOpposite.instDivisionSemiring α; let __src_1 := MulOpposite.instCommSemiring α; Semifield.mk ⋯ DivisionSemiring.zpow ⋯ ⋯ ⋯ ⋯ ⋯

instance MulOpposite.instField (α : Type u_1) [Field α] : Field αᵐᵒᵖ

Equations

• MulOpposite.instField α = let __src := MulOpposite.instDivisionRing α; let __src_1 := MulOpposite.instCommRing α; Field.mk ⋯ DivisionRing.zpow ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ DivisionRing.qsmul ⋯

instance AddOpposite.instDivisionSemiring {α : Type u_1} [DivisionSemiring α] : DivisionSemiring αᵃᵒᵖ

Equations

• AddOpposite.instDivisionSemiring = let __src := AddOpposite.instGroupWithZero α; let __src_1 := AddOpposite.instSemiring α; DivisionSemiring.mk ⋯ GroupWithZero.zpow ⋯ ⋯ ⋯ ⋯ ⋯

instance AddOpposite.instDivisionRing {α : Type u_1} [DivisionRing α] : DivisionRing αᵃᵒᵖ

Equations

• One or more equations did not get rendered due to their size.

instance AddOpposite.instSemifield {α : Type u_1} [Semifield α] : Semifield αᵃᵒᵖ

Equations

• AddOpposite.instSemifield = let __src := AddOpposite.instDivisionSemiring; let __src_1 := AddOpposite.instCommSemiring α; Semifield.mk ⋯ DivisionSemiring.zpow ⋯ ⋯ ⋯ ⋯ ⋯

instance AddOpposite.instField {α : Type u_1} [Field α] : Field αᵃᵒᵖ

Equations

• AddOpposite.instField = let __src := AddOpposite.instDivisionRing; let __src_1 := AddOpposite.instCommRing α; Field.mk ⋯ DivisionRing.zpow ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ DivisionRing.qsmul ⋯