Loogle!

Result

Found 44 declarations mentioning MvPolynomial.IsHomogeneous.

• MvPolynomial.IsHomogeneous 📋 Mathlib.RingTheory.MvPolynomial.Homogeneous
  {σ : Type u_1} {R : Type u_3} [CommSemiring R] (φ : MvPolynomial σ R) (n : ℕ) : Prop
• MvPolynomial.isHomogeneous_X 📋 Mathlib.RingTheory.MvPolynomial.Homogeneous
  {σ : Type u_1} (R : Type u_3) [CommSemiring R] (i : σ) : (MvPolynomial.X i).IsHomogeneous 1
• MvPolynomial.IsHomogeneous.totalDegree_le 📋 Mathlib.RingTheory.MvPolynomial.Homogeneous
  {σ : Type u_1} {R : Type u_3} [CommSemiring R] {φ : MvPolynomial σ R} {n : ℕ} (hφ : φ.IsHomogeneous n) : φ.totalDegree ≤ n
• MvPolynomial.isHomogeneous_of_totalDegree_zero 📋 Mathlib.RingTheory.MvPolynomial.Homogeneous
  (σ : Type u_1) {R : Type u_3} [CommSemiring R] {p : MvPolynomial σ R} : p.totalDegree = 0 → p.IsHomogeneous 0
• MvPolynomial.totalDegree_zero_iff_isHomogeneous 📋 Mathlib.RingTheory.MvPolynomial.Homogeneous
  (σ : Type u_1) {R : Type u_3} [CommSemiring R] {p : MvPolynomial σ R} : p.totalDegree = 0 ↔ p.IsHomogeneous 0
• MvPolynomial.IsHomogeneous.eq_1 📋 Mathlib.RingTheory.MvPolynomial.Homogeneous
  {σ : Type u_1} {R : Type u_3} [CommSemiring R] (φ : MvPolynomial σ R) (n : ℕ) : φ.IsHomogeneous n = MvPolynomial.IsWeightedHomogeneous 1 φ n
• MvPolynomial.isHomogeneous_zero 📋 Mathlib.RingTheory.MvPolynomial.Homogeneous
  (σ : Type u_1) (R : Type u_3) [CommSemiring R] (n : ℕ) : MvPolynomial.IsHomogeneous 0 n
• MvPolynomial.isHomogeneous_one 📋 Mathlib.RingTheory.MvPolynomial.Homogeneous
  (σ : Type u_1) (R : Type u_3) [CommSemiring R] : MvPolynomial.IsHomogeneous 1 0
• MvPolynomial.IsHomogeneous.coeff_eq_zero 📋 Mathlib.RingTheory.MvPolynomial.Homogeneous
  {σ : Type u_1} {R : Type u_3} [CommSemiring R] {φ : MvPolynomial σ R} {n : ℕ} (hφ : φ.IsHomogeneous n) {d : σ →₀ ℕ} (hd : d.degree ≠ n) : MvPolynomial.coeff d φ = 0
• MvPolynomial.isHomogeneous_X_pow 📋 Mathlib.RingTheory.MvPolynomial.Homogeneous
  {σ : Type u_1} {R : Type u_3} [CommSemiring R] (i : σ) (n : ℕ) : (MvPolynomial.X i ^ n).IsHomogeneous n
• MvPolynomial.IsHomogeneous.prod 📋 Mathlib.RingTheory.MvPolynomial.Homogeneous
  {σ : Type u_1} {R : Type u_3} [CommSemiring R] {ι : Type u_5} (s : Finset ι) (φ : ι → MvPolynomial σ R) (n : ι → ℕ) (h : ∀ i ∈ s, (φ i).IsHomogeneous (n i)) : (∏ i ∈ s, φ i).IsHomogeneous (∑ i ∈ s, n i)
• MvPolynomial.IsHomogeneous.sum 📋 Mathlib.RingTheory.MvPolynomial.Homogeneous
  {σ : Type u_1} {R : Type u_3} [CommSemiring R] {ι : Type u_5} (s : Finset ι) (φ : ι → MvPolynomial σ R) (n : ℕ) (h : ∀ i ∈ s, (φ i).IsHomogeneous n) : (∑ i ∈ s, φ i).IsHomogeneous n
• MvPolynomial.IsHomogeneous.totalDegree 📋 Mathlib.RingTheory.MvPolynomial.Homogeneous
  {σ : Type u_1} {R : Type u_3} [CommSemiring R] {φ : MvPolynomial σ R} {n : ℕ} (hφ : φ.IsHomogeneous n) (h : φ ≠ 0) : φ.totalDegree = n
• MvPolynomial.IsHomogeneous.pow 📋 Mathlib.RingTheory.MvPolynomial.Homogeneous
  {σ : Type u_1} {R : Type u_3} [CommSemiring R] {φ : MvPolynomial σ R} {m : ℕ} (hφ : φ.IsHomogeneous m) (n : ℕ) : (φ ^ n).IsHomogeneous (m * n)
• MvPolynomial.IsHomogeneous.inj_right 📋 Mathlib.RingTheory.MvPolynomial.Homogeneous
  {σ : Type u_1} {R : Type u_3} [CommSemiring R] {φ : MvPolynomial σ R} {m n : ℕ} (hm : φ.IsHomogeneous m) (hn : φ.IsHomogeneous n) (hφ : φ ≠ 0) : m = n
• MvPolynomial.isHomogeneous_C 📋 Mathlib.RingTheory.MvPolynomial.Homogeneous
  (σ : Type u_1) {R : Type u_3} [CommSemiring R] (r : R) : (MvPolynomial.C r).IsHomogeneous 0
• MvPolynomial.IsHomogeneous.add 📋 Mathlib.RingTheory.MvPolynomial.Homogeneous
  {σ : Type u_1} {R : Type u_3} [CommSemiring R] {φ ψ : MvPolynomial σ R} {n : ℕ} (hφ : φ.IsHomogeneous n) (hψ : ψ.IsHomogeneous n) : (φ + ψ).IsHomogeneous n
• MvPolynomial.IsHomogeneous.neg 📋 Mathlib.RingTheory.MvPolynomial.Homogeneous
  {R : Type u_5} {σ : Type u_6} [CommRing R] {φ : MvPolynomial σ R} {n : ℕ} (hφ : φ.IsHomogeneous n) : (-φ).IsHomogeneous n
• MvPolynomial.IsHomogeneous.mul 📋 Mathlib.RingTheory.MvPolynomial.Homogeneous
  {σ : Type u_1} {R : Type u_3} [CommSemiring R] {φ ψ : MvPolynomial σ R} {m n : ℕ} (hφ : φ.IsHomogeneous m) (hψ : ψ.IsHomogeneous n) : (φ * ψ).IsHomogeneous (m + n)
• MvPolynomial.IsHomogeneous.sub 📋 Mathlib.RingTheory.MvPolynomial.Homogeneous
  {R : Type u_5} {σ : Type u_6} [CommRing R] {φ ψ : MvPolynomial σ R} {n : ℕ} (hφ : φ.IsHomogeneous n) (hψ : ψ.IsHomogeneous n) : (φ - ψ).IsHomogeneous n
• MvPolynomial.isHomogeneous_C_mul_X 📋 Mathlib.RingTheory.MvPolynomial.Homogeneous
  {σ : Type u_1} {R : Type u_3} [CommSemiring R] (r : R) (i : σ) : (MvPolynomial.C r * MvPolynomial.X i).IsHomogeneous 1
• MvPolynomial.IsHomogeneous.C_mul 📋 Mathlib.RingTheory.MvPolynomial.Homogeneous
  {σ : Type u_1} {R : Type u_3} [CommSemiring R] {φ : MvPolynomial σ R} {m : ℕ} (hφ : φ.IsHomogeneous m) (r : R) : (MvPolynomial.C r * φ).IsHomogeneous m
• MvPolynomial.IsHomogeneous.map 📋 Mathlib.RingTheory.MvPolynomial.Homogeneous
  {σ : Type u_1} {R : Type u_3} {S : Type u_4} [CommSemiring R] [CommSemiring S] {φ : MvPolynomial σ R} {n : ℕ} (hφ : φ.IsHomogeneous n) (f : R →+* S) : ((MvPolynomial.map f) φ).IsHomogeneous n
• MvPolynomial.IsHomogeneous.rename_isHomogeneous 📋 Mathlib.RingTheory.MvPolynomial.Homogeneous
  {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [CommSemiring R] {φ : MvPolynomial σ R} {n : ℕ} {f : σ → τ} (h : φ.IsHomogeneous n) : ((MvPolynomial.rename f) φ).IsHomogeneous n
• MvPolynomial.IsHomogeneous.rename_isHomogeneous_iff 📋 Mathlib.RingTheory.MvPolynomial.Homogeneous
  {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [CommSemiring R] {φ : MvPolynomial σ R} {n : ℕ} {f : σ → τ} (hf : Function.Injective f) : ((MvPolynomial.rename f) φ).IsHomogeneous n ↔ φ.IsHomogeneous n
• MvPolynomial.IsHomogeneous.eval₂ 📋 Mathlib.RingTheory.MvPolynomial.Homogeneous
  {σ : Type u_1} {τ : Type u_2} {R : Type u_3} {S : Type u_4} [CommSemiring R] [CommSemiring S] {φ : MvPolynomial σ R} {m n : ℕ} (hφ : φ.IsHomogeneous m) (f : R →+* MvPolynomial τ S) (g : σ → MvPolynomial τ S) (hf : ∀ (r : R), (f r).IsHomogeneous 0) (hg : ∀ (i : σ), (g i).IsHomogeneous n) : (MvPolynomial.eval₂ f g φ).IsHomogeneous (n * m)
• MvPolynomial.isHomogeneous_C_mul_X_pow 📋 Mathlib.RingTheory.MvPolynomial.Homogeneous
  {σ : Type u_1} {R : Type u_3} [CommSemiring R] (r : R) (i : σ) (n : ℕ) : (MvPolynomial.C r * MvPolynomial.X i ^ n).IsHomogeneous n
• MvPolynomial.mem_homogeneousSubmodule 📋 Mathlib.RingTheory.MvPolynomial.Homogeneous
  {σ : Type u_1} {R : Type u_3} [CommSemiring R] (n : ℕ) (p : MvPolynomial σ R) : p ∈ MvPolynomial.homogeneousSubmodule σ R n ↔ p.IsHomogeneous n
• MvPolynomial.IsHomogeneous.aeval 📋 Mathlib.RingTheory.MvPolynomial.Homogeneous
  {σ : Type u_1} {τ : Type u_2} {R : Type u_3} {S : Type u_4} [CommSemiring R] [CommSemiring S] {φ : MvPolynomial σ R} {m n : ℕ} [Algebra R S] (hφ : φ.IsHomogeneous m) (g : σ → MvPolynomial τ S) (hg : ∀ (i : σ), (g i).IsHomogeneous n) : ((MvPolynomial.aeval g) φ).IsHomogeneous (n * m)
• MvPolynomial.isHomogeneous_monomial 📋 Mathlib.RingTheory.MvPolynomial.Homogeneous
  {σ : Type u_1} {R : Type u_3} [CommSemiring R] {d : σ →₀ ℕ} (r : R) {n : ℕ} (hn : d.degree = n) : ((MvPolynomial.monomial d) r).IsHomogeneous n
• MvPolynomial.IsHomogeneous.eq_zero_of_forall_eval_eq_zero 📋 Mathlib.RingTheory.MvPolynomial.Homogeneous
  {R : Type u_5} {σ : Type u_6} [CommRing R] [IsDomain R] [Infinite R] {F : MvPolynomial σ R} {n : ℕ} (hF : F.IsHomogeneous n) (h : ∀ (r : σ → R), (MvPolynomial.eval r) F = 0) : F = 0
• MvPolynomial.IsHomogeneous.eq_zero_of_forall_eval_eq_zero_of_le_card 📋 Mathlib.RingTheory.MvPolynomial.Homogeneous
  {R : Type u_5} {σ : Type u_6} [CommRing R] [IsDomain R] {F : MvPolynomial σ R} {n : ℕ} (hF : F.IsHomogeneous n) (h : ∀ (r : σ → R), (MvPolynomial.eval r) F = 0) (hnR : ↑n ≤ Cardinal.mk R) : F = 0
• MvPolynomial.homogeneousComponent_isHomogeneous 📋 Mathlib.RingTheory.MvPolynomial.Homogeneous
  {σ : Type u_1} {R : Type u_3} [CommSemiring R] (n : ℕ) (φ : MvPolynomial σ R) : ((MvPolynomial.homogeneousComponent n) φ).IsHomogeneous n
• MvPolynomial.IsHomogeneous.funext 📋 Mathlib.RingTheory.MvPolynomial.Homogeneous
  {R : Type u_5} {σ : Type u_6} [CommRing R] [IsDomain R] [Infinite R] {F G : MvPolynomial σ R} {n : ℕ} (hF : F.IsHomogeneous n) (hG : G.IsHomogeneous n) (h : ∀ (r : σ → R), (MvPolynomial.eval r) F = (MvPolynomial.eval r) G) : F = G
• MvPolynomial.IsHomogeneous.funext_of_le_card 📋 Mathlib.RingTheory.MvPolynomial.Homogeneous
  {R : Type u_5} {σ : Type u_6} [CommRing R] [IsDomain R] {F G : MvPolynomial σ R} {n : ℕ} (hF : F.IsHomogeneous n) (hG : G.IsHomogeneous n) (h : ∀ (r : σ → R), (MvPolynomial.eval r) F = (MvPolynomial.eval r) G) (hnR : ↑n ≤ Cardinal.mk R) : F = G
• MvPolynomial.IsHomogeneous.coeff_isHomogeneous_of_optionEquivLeft_symm 📋 Mathlib.RingTheory.MvPolynomial.Homogeneous
  {σ : Type u_1} {R : Type u_3} [CommSemiring R] {n : ℕ} [hσ : Finite σ] {p : Polynomial (MvPolynomial σ R)} (hp : ((MvPolynomial.optionEquivLeft R σ).symm p).IsHomogeneous n) (i j : ℕ) (h : i + j = n) : (p.coeff i).IsHomogeneous j
• MvPolynomial.IsHomogeneous.finSuccEquiv_coeff_isHomogeneous 📋 Mathlib.RingTheory.MvPolynomial.Homogeneous
  {R : Type u_3} [CommSemiring R] {N : ℕ} {φ : MvPolynomial (Fin (N + 1)) R} {n : ℕ} (hφ : φ.IsHomogeneous n) (i j : ℕ) (h : i + j = n) : (((MvPolynomial.finSuccEquiv R N) φ).coeff i).IsHomogeneous j
• Matrix.charpoly.univ_coeff_isHomogeneous 📋 Mathlib.LinearAlgebra.Matrix.Charpoly.Univ
  (R : Type u_1) (n : Type u_3) [CommRing R] [Fintype n] [DecidableEq n] (i j : ℕ) (h : i + j = Fintype.card n) : ((Matrix.charpoly.univ R n).coeff i).IsHomogeneous j
• Matrix.charpoly.optionEquivLeft_symm_univ_isHomogeneous 📋 Mathlib.LinearAlgebra.Matrix.Charpoly.Univ
  (R : Type u_1) (n : Type u_3) [CommRing R] [Fintype n] [DecidableEq n] : ((MvPolynomial.optionEquivLeft R (n × n)).symm (Matrix.charpoly.univ R n)).IsHomogeneous (Fintype.card n)
• Matrix.toMvPolynomial_isHomogeneous 📋 Mathlib.Algebra.Module.LinearMap.Polynomial
  {m : Type u_1} {n : Type u_2} {R : Type u_4} [Fintype n] [CommSemiring R] (M : Matrix m n R) (i : m) : (M.toMvPolynomial i).IsHomogeneous 1
• LinearMap.toMvPolynomial_isHomogeneous 📋 Mathlib.Algebra.Module.LinearMap.Polynomial
  {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} {ι₁ : Type u_4} {ι₂ : Type u_5} [CommRing R] [AddCommGroup M₁] [AddCommGroup M₂] [Module R M₁] [Module R M₂] [Fintype ι₁] [Finite ι₂] [DecidableEq ι₁] (b₁ : Basis ι₁ R M₁) (b₂ : Basis ι₂ R M₂) (f : M₁ →ₗ[R] M₂) (i : ι₂) : (LinearMap.toMvPolynomial b₁ b₂ f i).IsHomogeneous 1
• LinearMap.polyCharpoly_coeff_isHomogeneous 📋 Mathlib.Algebra.Module.LinearMap.Polynomial
  {R : Type u_1} {L : Type u_2} {M : Type u_3} {ι : Type u_5} [CommRing R] [AddCommGroup L] [Module R L] [AddCommGroup M] [Module R M] (φ : L →ₗ[R] Module.End R M) [Fintype ι] [DecidableEq ι] [Module.Free R M] [Module.Finite R M] (b : Basis ι R L) (i j : ℕ) (hij : i + j = Module.finrank R M) [Nontrivial R] : ((φ.polyCharpoly b).coeff i).IsHomogeneous j
• MvPolynomial.IsHomogeneous.pderiv 📋 Mathlib.RingTheory.MvPolynomial.EulerIdentity
  {R : Type u_1} {σ : Type u_2} [CommSemiring R] {φ : MvPolynomial σ R} {n : ℕ} {i : σ} (h : φ.IsHomogeneous n) : ((MvPolynomial.pderiv i) φ).IsHomogeneous (n - 1)
• MvPolynomial.IsHomogeneous.sum_X_mul_pderiv 📋 Mathlib.RingTheory.MvPolynomial.EulerIdentity
  {R : Type u_1} {σ : Type u_2} [CommSemiring R] {φ : MvPolynomial σ R} [Fintype σ] {n : ℕ} (h : φ.IsHomogeneous n) : ∑ i, MvPolynomial.X i * (MvPolynomial.pderiv i) φ = n • φ

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using (by default) Ctrl-K Ctrl-S. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO.

This is Loogle revision 19971e9 serving mathlib revision 4cb993b