Theorems · Theorem · number theory
jacobiSym.pow_right
∀ (a : ℤ) (b e : ℕ), jacobiSym a (b ^ e) = jacobiSym a b ^ e
We have that J(a | b^e) = J(a | b)^e.
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 149 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- pow_zeroproof · cited by 1,094
- one_powproof · cited by 521
- pow_succproof · cited by 374
- zero_powproof · cited by 361
- jacobiSymstatement and proof · cited by 44
- eq_zero_or_neZeroproof · cited by 36
- jacobiSym.zero_rightproof · cited by 4
- jacobiSym.mul_rightproof · cited by 2
- jacobiSym.one_rightproof · cited by 2
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.