Lemmas for the field_simp tactic #
This is a variant of integer exponentiation, defined for internal use in the field_simp
tactic
implementation. It differs from the usual integer exponentiation in that 0 ^ 0
is 0
, not 1
.
With this choice, the function n ↦ a ^ n
is always a homomorphism (a ^ (n + m) = a ^ n * a ^ m
),
even if a
is zero.
Instances For
Theory of lists of pairs (exponent, atom) #
This section contains the lemmas which are orchestrated by the field_simp
tactic
to prove goals in fields. The basic object which these lemmas concern is NF M
, a type synonym
for a list of ordered pairs in ℤ × M
, where typically M
is a field.
Basic theoretical "normal form" object of the field_simp
tactic: a type
synonym for a list of ordered pairs in ℤ × M
, where typically M
is a field. This is the
form to which the tactics reduce field expressions.
Equations
- Mathlib.Tactic.FieldSimp.NF M = List (ℤ × M)
Instances For
Augment a FieldSimp.NF M
object l
, i.e. a list of pairs in ℤ × M
, by prepending another
pair p : ℤ × M
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Evaluate a FieldSimp.NF M
object l
, i.e. a list of pairs in ℤ × M
, to an element of M
,
by forming the "multiplicative linear combination" it specifies: raise each M
term to the power of
the corresponding ℤ
term, then multiply them all together.
Equations
Instances For
Equations
- One or more equations did not get rendered due to their size.
Negations of algebraic operations #
Inductive type representing the options for the sign of an element in a type-expression M
If the sign is "-", then we also carry an expression for a field instance on M
, to allow us to
construct that negation when needed.
- plus {v : Lean.Level} {M : Q(Type v)} : Sign M
- minus {v : Lean.Level} {M : Q(Type v)} (iM : Q(Field «$M»)) : Sign M
Instances For
Given an expression e : Q($M)
, construct an expression which is morally "± e
", with the
choice between + and - determined by an object g : Sign M
.
Equations
- Mathlib.Tactic.FieldSimp.Sign.plus.expr x✝ = x✝
- (Mathlib.Tactic.FieldSimp.Sign.minus iM).expr x✝ = q(-$x✝)
Instances For
Given an expression y : Q($M)
with specified sign (either + or -), construct a proof that
the product with c
of (± y
) (here taking the specified sign) is ± c * y
.
Equations
Instances For
Given expressions y₁ y₂ : Q($M)
with specified signs (either + or -), construct a proof that
the product of (± y₁
) and (± y₂
) (here taking the specified signs) is ± y₁ * y₂
; return this
proof and the computed sign.
Equations
- Mathlib.Tactic.FieldSimp.Sign.mul iM y₁ y₂ Mathlib.Tactic.FieldSimp.Sign.plus Mathlib.Tactic.FieldSimp.Sign.plus = pure ⟨Mathlib.Tactic.FieldSimp.Sign.plus, q(⋯)⟩
- Mathlib.Tactic.FieldSimp.Sign.mul iM y₁ y₂ Mathlib.Tactic.FieldSimp.Sign.plus (Mathlib.Tactic.FieldSimp.Sign.minus i) = pure ⟨Mathlib.Tactic.FieldSimp.Sign.minus i, q(⋯)⟩
- Mathlib.Tactic.FieldSimp.Sign.mul iM y₁ y₂ (Mathlib.Tactic.FieldSimp.Sign.minus i) Mathlib.Tactic.FieldSimp.Sign.plus = pure ⟨Mathlib.Tactic.FieldSimp.Sign.minus i, q(⋯)⟩
- Mathlib.Tactic.FieldSimp.Sign.mul iM y₁ y₂ (Mathlib.Tactic.FieldSimp.Sign.minus iM_1) (Mathlib.Tactic.FieldSimp.Sign.minus iM_2) = pure ⟨Mathlib.Tactic.FieldSimp.Sign.plus, q(⋯)⟩
Instances For
Given an expression y : Q($M)
with specified sign (either + or -), construct a proof that
the inverse of (± y
) (here taking the specified sign) is ± y⁻¹
.
Equations
Instances For
Given expressions y₁ y₂ : Q($M)
with specified signs (either + or -), construct a proof that
the quotient of (± y₁
) and (± y₂
) (here taking the specified signs) is ± y₁ / y₂
; return this
proof and the computed sign.
Equations
- Mathlib.Tactic.FieldSimp.Sign.div iM y₁ y₂ Mathlib.Tactic.FieldSimp.Sign.plus Mathlib.Tactic.FieldSimp.Sign.plus = pure ⟨Mathlib.Tactic.FieldSimp.Sign.plus, q(⋯)⟩
- Mathlib.Tactic.FieldSimp.Sign.div iM y₁ y₂ Mathlib.Tactic.FieldSimp.Sign.plus (Mathlib.Tactic.FieldSimp.Sign.minus i) = pure ⟨Mathlib.Tactic.FieldSimp.Sign.minus i, q(⋯)⟩
- Mathlib.Tactic.FieldSimp.Sign.div iM y₁ y₂ (Mathlib.Tactic.FieldSimp.Sign.minus i) Mathlib.Tactic.FieldSimp.Sign.plus = pure ⟨Mathlib.Tactic.FieldSimp.Sign.minus i, q(⋯)⟩
- Mathlib.Tactic.FieldSimp.Sign.div iM y₁ y₂ (Mathlib.Tactic.FieldSimp.Sign.minus iM_1) (Mathlib.Tactic.FieldSimp.Sign.minus iM_2) = pure ⟨Mathlib.Tactic.FieldSimp.Sign.plus, q(⋯)⟩
Instances For
Given an expression y : Q($M)
with specified sign (either + or -), construct a proof that
the negation of (± y
) (here taking the specified sign) is ∓ y
.
Equations
Instances For
Given an expression y : Q($M)
with specified sign (either + or -), construct a proof that
the exponentiation to power s : ℕ
of (± y
) (here taking the specified signs) is ± y ^ s
;
return this proof and the computed sign.
Equations
- One or more equations did not get rendered due to their size.
- Mathlib.Tactic.FieldSimp.Sign.pow iM y Mathlib.Tactic.FieldSimp.Sign.plus s = pure ⟨Mathlib.Tactic.FieldSimp.Sign.plus, q(⋯)⟩
Instances For
Given an expression y : Q($M)
with specified sign (either + or -), construct a proof that
the exponentiation to power s : ℤ
of (± y
) (here taking the specified signs) is ± y ^ s
;
return this proof and the computed sign.
Equations
- One or more equations did not get rendered due to their size.
- Mathlib.Tactic.FieldSimp.Sign.zpow iM y Mathlib.Tactic.FieldSimp.Sign.plus s = pure ⟨Mathlib.Tactic.FieldSimp.Sign.plus, q(⋯)⟩
Instances For
Given a proof that two expressions y₁ y₂ : Q($M)
are equal, construct a proof that (± y₁
)
and (± y₂
) are equal, where the same sign is taken in both expression.
Equations
- Mathlib.Tactic.FieldSimp.Sign.plus.congr pf = pf
- (Mathlib.Tactic.FieldSimp.Sign.minus iM).congr pf = q(⋯)
Instances For
If a
= ± b
, b = C * d
, and d = e
, construct a proof that a
= C
* ± e
.
Equations
- One or more equations did not get rendered due to their size.