Theorems · Theorem · commutative algebra

Polynomial.degreeLT.addLinearEquiv_natAdd

∀ {R : Type u_1} [inst : Semiring R] {m n : ℕ} (i : Fin n),
  (Polynomial.degreeLT.addLinearEquiv R m n) ((Polynomial.degreeLT.basis R (m + n)) (Fin.natAdd m i)) =
    (0, (Polynomial.degreeLT.basis R n) i)

Defined in: Mathlib.RingTheory.Polynomial.DegreeLT
Cited by: 1 results in Mathlib
Foundations: Depth 109 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Semiring

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites15

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coestatement and proof · cited by 62,936
RingHom.idstatement and proof · cited by 18,349
Semiringstatement and proof · cited by 13,802
Submodulestatement · cited by 7,192
Polynomialstatement and proof · cited by 5,681
LinearEquivstatement and proof · cited by 3,317
Module.Basisstatement · cited by 1,477
Equiv.reflproof · cited by 274
Polynomial.degreeLTstatement and proof · cited by 47
Polynomial.degreeLT.basisstatement and proof · cited by 15
Module.Basis.equiv_applyproof · cited by 13
Polynomial.degreeLT.addLinearEquivstatement · cited by 12

Cited by1

Results whose statement or proof uses this declaration.

Polynomial.degreeLT.addLinearEquiv_symm_apply_inr_basisproof · cited by 1