Loogle!

Result

Found 107 declarations mentioning NonUnitalAlgHomClass.

• NonUnitalAlgHomClass 📋 Mathlib.Algebra.Algebra.NonUnitalHom
  (F : Type u_1) (R : outParam (Type u_2)) (A : outParam (Type u_3)) (B : outParam (Type u_4)) [Monoid R] [NonUnitalNonAssocSemiring A] [NonUnitalNonAssocSemiring B] [DistribMulAction R A] [DistribMulAction R B] [FunLike F A B] : Prop
• NonUnitalAlgHomClass.toNonUnitalAlgHom 📋 Mathlib.Algebra.Algebra.NonUnitalHom
  {F : Type u_3} {R : Type u_4} [Monoid R] {A : Type u_5} {B : Type u_6} [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] (f : F) : A →ₙₐ[R] B
• NonUnitalAlgHomClass.instCoeTCNonUnitalAlgHomId 📋 Mathlib.Algebra.Algebra.NonUnitalHom
  {F : Type u_3} {R : Type u_4} [Monoid R] {A : Type u_5} {B : Type u_6} [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] : CoeTC F (A →ₙₐ[R] B)
• NonUnitalAlgHomClass.instLinearMapClass 📋 Mathlib.Algebra.Algebra.NonUnitalHom
  {R : Type u} [Semiring R] {A : Type u_1} {B : Type u_2} [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] {F : Type u_3} [FunLike F A B] [Module R B] [NonUnitalAlgHomClass F R A B] : LinearMapClass F R A B
• AlgHom.instNonUnitalAlgHomClassOfAlgHomClass 📋 Mathlib.Algebra.Algebra.NonUnitalHom
  {F : Type u_1} {R : Type u_2} [CommSemiring R] {A : Type u_3} {B : Type u_4} [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [FunLike F A B] [AlgHomClass F R A B] : NonUnitalAlgHomClass F R A B
• NonUnitalAlgHom.range 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] (φ : F) : NonUnitalSubalgebra R B
• NonUnitalAlgHom.equalizer 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] (ϕ ψ : F) : NonUnitalSubalgebra R A
• NonUnitalSubalgebra.comap 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [NonUnitalNonAssocSemiring B] [Module R A] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] (f : F) (S : NonUnitalSubalgebra R B) : NonUnitalSubalgebra R A
• NonUnitalSubalgebra.map 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [NonUnitalNonAssocSemiring B] [Module R A] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] (f : F) (S : NonUnitalSubalgebra R A) : NonUnitalSubalgebra R B
• NonUnitalSubalgebra.map_injective 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [NonUnitalNonAssocSemiring B] [Module R A] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] {f : F} (hf : Function.Injective ⇑f) : Function.Injective (NonUnitalSubalgebra.map f)
• NonUnitalAlgHom.coe_range 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] (φ : F) : ↑(NonUnitalAlgHom.range φ) = Set.range ⇑φ
• NonUnitalAlgHom.fintypeRange 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [Fintype A] [DecidableEq B] (φ : F) : Fintype ↥(NonUnitalAlgHom.range φ)
• NonUnitalAlgHom.mem_range_self 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] (φ : F) (x : A) : φ x ∈ NonUnitalAlgHom.range φ
• NonUnitalAlgHom.mem_range 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] (φ : F) {y : B} : y ∈ NonUnitalAlgHom.range φ ↔ ∃ x, φ x = y
• NonUnitalAlgHom.mem_equalizer 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] (φ ψ : F) (x : A) : x ∈ NonUnitalAlgHom.equalizer φ ψ ↔ φ x = ψ x
• NonUnitalSubalgebra.coe_comap 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [NonUnitalNonAssocSemiring B] [Module R A] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] (S : NonUnitalSubalgebra R B) (f : F) : ↑(NonUnitalSubalgebra.comap f S) = ⇑f ⁻¹' ↑S
• NonUnitalSubalgebra.coe_map 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [NonUnitalNonAssocSemiring B] [Module R A] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] (S : NonUnitalSubalgebra R A) (f : F) : ↑(NonUnitalSubalgebra.map f S) = ⇑f '' ↑S
• NonUnitalSubalgebra.gc_map_comap 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [NonUnitalNonAssocSemiring B] [Module R A] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] (f : F) : GaloisConnection (NonUnitalSubalgebra.map f) (NonUnitalSubalgebra.comap f)
• NonUnitalSubalgebra.mem_comap 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [NonUnitalNonAssocSemiring B] [Module R A] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] (S : NonUnitalSubalgebra R B) (f : F) (x : A) : x ∈ NonUnitalSubalgebra.comap f S ↔ f x ∈ S
• NonUnitalSubalgebra.mem_map 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [NonUnitalNonAssocSemiring B] [Module R A] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] {S : NonUnitalSubalgebra R A} {f : F} {y : B} : y ∈ NonUnitalSubalgebra.map f S ↔ ∃ x ∈ S, f x = y
• NonUnitalSubalgebra.map_mono 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [NonUnitalNonAssocSemiring B] [Module R A] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] {S₁ S₂ : NonUnitalSubalgebra R A} {f : F} : S₁ ≤ S₂ → NonUnitalSubalgebra.map f S₁ ≤ NonUnitalSubalgebra.map f S₂
• NonUnitalSubalgebra.map_le 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [NonUnitalNonAssocSemiring B] [Module R A] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] {S : NonUnitalSubalgebra R A} {f : F} {U : NonUnitalSubalgebra R B} : NonUnitalSubalgebra.map f S ≤ U ↔ S ≤ NonUnitalSubalgebra.comap f U
• NonUnitalSubalgebra.map_toSubmodule 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [NonUnitalNonAssocSemiring B] [Module R A] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] {S : NonUnitalSubalgebra R A} {f : F} : (NonUnitalSubalgebra.map f S).toSubmodule = Submodule.map (LinearMapClass.linearMap f) S.toSubmodule
• NonUnitalSubalgebra.map_toNonUnitalSubsemiring 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [NonUnitalNonAssocSemiring B] [Module R A] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] {S : NonUnitalSubalgebra R A} {f : F} : (NonUnitalSubalgebra.map f S).toNonUnitalSubsemiring = NonUnitalSubsemiring.map (↑f) S.toNonUnitalSubsemiring
• NonUnitalAlgHom.codRestrict 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] (f : F) (S : NonUnitalSubalgebra R B) (hf : ∀ (x : A), f x ∈ S) : A →ₙₐ[R] ↥S
• NonUnitalAlgHom.rangeRestrict 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] (f : F) : A →ₙₐ[R] ↥(NonUnitalAlgHom.range f)
• NonUnitalAlgHom.map_adjoin 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {F : Type u_1} (R : Type u) (A : Type v) {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [IsScalarTower R A A] [SMulCommClass R A A] [IsScalarTower R B B] [SMulCommClass R B B] (f : F) (s : Set A) : NonUnitalSubalgebra.map f (NonUnitalAlgebra.adjoin R s) = NonUnitalAlgebra.adjoin R (⇑f '' s)
• NonUnitalAlgHom.map_adjoin_singleton 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {F : Type u_1} (R : Type u) (A : Type v) {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [IsScalarTower R A A] [SMulCommClass R A A] [IsScalarTower R B B] [SMulCommClass R B B] (f : F) (x : A) : NonUnitalSubalgebra.map f (NonUnitalAlgebra.adjoin R {x}) = NonUnitalAlgebra.adjoin R {f x}
• NonUnitalSubalgebra.map_center_eq 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u_1} {A : Type u_2} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {B : Type u_3} {F : Type u_4} [NonUnitalNonAssocSemiring B] [Module R B] [IsScalarTower R B B] [SMulCommClass R B B] [EquivLike F A B] [NonUnitalAlgHomClass F R A B] (f : F) : NonUnitalSubalgebra.map f (NonUnitalSubalgebra.center R A) = NonUnitalSubalgebra.center R B
• NonUnitalAlgHom.coe_codRestrict 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] (f : F) (S : NonUnitalSubalgebra R B) (hf : ∀ (x : A), f x ∈ S) (x : A) : ↑((NonUnitalAlgHom.codRestrict f S hf) x) = f x
• NonUnitalAlgHom.injective_codRestrict 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] (f : F) (S : NonUnitalSubalgebra R B) (hf : ∀ (x : A), f x ∈ S) : Function.Injective ⇑(NonUnitalAlgHom.codRestrict f S hf) ↔ Function.Injective ⇑f
• NonUnitalSubalgebra.map_center_le_center 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u_1} {A : Type u_2} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {B : Type u_3} {F : Type u_4} [NonUnitalNonAssocSemiring B] [Module R B] [IsScalarTower R B B] [SMulCommClass R B B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] {f : F} (hf : Function.Surjective ⇑f) : NonUnitalSubalgebra.map f (NonUnitalSubalgebra.center R A) ≤ NonUnitalSubalgebra.center R B
• NonUnitalSubalgebra.comap_center_le_center 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u_1} {A : Type u_2} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {B : Type u_3} {F : Type u_4} [NonUnitalNonAssocSemiring B] [Module R B] [IsScalarTower R B B] [SMulCommClass R B B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] {f : F} (hf : Function.Injective ⇑f) : NonUnitalSubalgebra.comap f (NonUnitalSubalgebra.center R B) ≤ NonUnitalSubalgebra.center R A
• NonUnitalAlgHom.subtype_comp_codRestrict 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] (f : F) (S : NonUnitalSubalgebra R B) (hf : ∀ (x : A), f x ∈ S) : (NonUnitalSubalgebraClass.subtype S).comp (NonUnitalAlgHom.codRestrict f S hf) = NonUnitalAlgHomClass.toNonUnitalAlgHom f
• NonUnitalAlgebra.map_iInf 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {F : Type u_1} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [IsScalarTower R A A] [SMulCommClass R A A] {ι : Sort u_2} [Nonempty ι] [IsScalarTower R B B] [SMulCommClass R B B] (f : F) (hf : Function.Injective ⇑f) (S : ι → NonUnitalSubalgebra R A) : NonUnitalSubalgebra.map f (⨅ i, S i) = ⨅ i, NonUnitalSubalgebra.map f (S i)
• NonUnitalAlgebra.map_sup 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {F : Type u_1} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [IsScalarTower R A A] [SMulCommClass R A A] [IsScalarTower R B B] [SMulCommClass R B B] (f : F) (S T : NonUnitalSubalgebra R A) : NonUnitalSubalgebra.map f (S ⊔ T) = NonUnitalSubalgebra.map f S ⊔ NonUnitalSubalgebra.map f T
• NonUnitalAlgebra.map_inf 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {F : Type u_1} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [IsScalarTower R A A] [SMulCommClass R A A] [IsScalarTower R B B] [SMulCommClass R B B] (f : F) (hf : Function.Injective ⇑f) (S T : NonUnitalSubalgebra R A) : NonUnitalSubalgebra.map f (S ⊓ T) = NonUnitalSubalgebra.map f S ⊓ NonUnitalSubalgebra.map f T
• NonUnitalStarAlgHom.instNonUnitalAlgHomClass 📋 Mathlib.Algebra.Star.StarAlgHom
  {R : Type u_1} {A : Type u_2} {B : Type u_3} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [Star A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [Star B] : NonUnitalAlgHomClass (A →⋆ₙₐ[R] B) R A B
• NonUnitalStarAlgHomClass.toNonUnitalStarAlgHom 📋 Mathlib.Algebra.Star.StarAlgHom
  {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [Star A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [Star B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [StarHomClass F A B] (f : F) : A →⋆ₙₐ[R] B
• NonUnitalStarAlgHomClass.instCoeTCNonUnitalStarAlgHomOfStarHomClass 📋 Mathlib.Algebra.Star.StarAlgHom
  {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [Star A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [Star B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [StarHomClass F A B] : CoeTC F (A →⋆ₙₐ[R] B)
• NonUnitalStarAlgHomClass.instNonUnitalStarRingHomClassOfStarHomClass 📋 Mathlib.Algebra.Star.StarAlgHom
  {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [Star A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [Star B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [StarHomClass F A B] : NonUnitalStarRingHomClass F A B
• NonUnitalStarAlgHom.coe_coe 📋 Mathlib.Algebra.Star.StarAlgHom
  {R : Type u_1} {A : Type u_2} {B : Type u_3} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [Star A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [Star B] {F : Type u_6} [FunLike F A B] [NonUnitalAlgHomClass F R A B] [StarHomClass F A B] (f : F) : ⇑↑f = ⇑f
• instNonUnitalAlgHomClassOfNonUnitalAlgEquivClass 📋 Mathlib.Algebra.Star.StarAlgHom
  {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [EquivLike F A B] [NonUnitalAlgEquivClass F R A B] : NonUnitalAlgHomClass F R A B
• StarAlgEquiv.ofBijective 📋 Mathlib.Algebra.Star.StarAlgHom
  {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [Star A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [Star B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [StarHomClass F A B] (f : F) (hf : Function.Bijective ⇑f) : A ≃⋆ₐ[R] B
• StarAlgEquiv.coe_ofBijective 📋 Mathlib.Algebra.Star.StarAlgHom
  {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [Star A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [Star B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [StarHomClass F A B] {f : F} (hf : Function.Bijective ⇑f) : ⇑(StarAlgEquiv.ofBijective f hf) = ⇑f
• StarAlgEquiv.ofBijective_apply 📋 Mathlib.Algebra.Star.StarAlgHom
  {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [Star A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [Star B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [StarHomClass F A B] {f : F} (hf : Function.Bijective ⇑f) (a : A) : (StarAlgEquiv.ofBijective f hf) a = f a
• NonUnitalStarAlgHom.range 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] [NonUnitalNonAssocSemiring B] [Module R B] [Star B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [StarHomClass F A B] (φ : F) : NonUnitalStarSubalgebra R B
• NonUnitalStarAlgHom.equalizer 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] [NonUnitalNonAssocSemiring B] [Module R B] [Star B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [StarHomClass F A B] (ϕ ψ : F) : NonUnitalStarSubalgebra R A
• NonUnitalStarSubalgebra.comap 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] [NonUnitalNonAssocSemiring B] [Module R B] [Star B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [StarHomClass F A B] (f : F) (S : NonUnitalStarSubalgebra R B) : NonUnitalStarSubalgebra R A
• NonUnitalStarSubalgebra.map 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] [NonUnitalNonAssocSemiring B] [Module R B] [Star B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [StarHomClass F A B] (f : F) (S : NonUnitalStarSubalgebra R A) : NonUnitalStarSubalgebra R B
• NonUnitalStarSubalgebra.map_injective 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] [NonUnitalNonAssocSemiring B] [Module R B] [Star B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [StarHomClass F A B] {f : F} (hf : Function.Injective ⇑f) : Function.Injective (NonUnitalStarSubalgebra.map f)
• NonUnitalStarAlgHom.coe_range 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] [NonUnitalNonAssocSemiring B] [Module R B] [Star B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [StarHomClass F A B] (φ : F) : ↑(NonUnitalStarAlgHom.range φ) = Set.range ⇑φ
• NonUnitalStarAlgHom.mem_range_self 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] [NonUnitalNonAssocSemiring B] [Module R B] [Star B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [StarHomClass F A B] (φ : F) (x : A) : φ x ∈ NonUnitalStarAlgHom.range φ
• NonUnitalStarAlgHom.mem_range 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] [NonUnitalNonAssocSemiring B] [Module R B] [Star B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [StarHomClass F A B] (φ : F) {y : B} : y ∈ NonUnitalStarAlgHom.range φ ↔ ∃ x, φ x = y
• NonUnitalStarSubalgebra.map_toNonUnitalSubalgebra 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] [NonUnitalNonAssocSemiring B] [Module R B] [Star B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [StarHomClass F A B] {S : NonUnitalStarSubalgebra R A} {f : F} : (NonUnitalStarSubalgebra.map f S).toNonUnitalSubalgebra = NonUnitalSubalgebra.map f S.toNonUnitalSubalgebra
• NonUnitalStarAlgHom.mem_equalizer 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] [NonUnitalNonAssocSemiring B] [Module R B] [Star B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [StarHomClass F A B] (φ ψ : F) (x : A) : x ∈ NonUnitalStarAlgHom.equalizer φ ψ ↔ φ x = ψ x
• NonUnitalStarSubalgebra.coe_comap 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] [NonUnitalNonAssocSemiring B] [Module R B] [Star B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [StarHomClass F A B] (S : NonUnitalStarSubalgebra R B) (f : F) : ↑(NonUnitalStarSubalgebra.comap f S) = ⇑f ⁻¹' ↑S
• NonUnitalStarSubalgebra.coe_map 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] [NonUnitalNonAssocSemiring B] [Module R B] [Star B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [StarHomClass F A B] (S : NonUnitalStarSubalgebra R A) (f : F) : ↑(NonUnitalStarSubalgebra.map f S) = ⇑f '' ↑S
• NonUnitalStarSubalgebra.gc_map_comap 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] [NonUnitalNonAssocSemiring B] [Module R B] [Star B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [StarHomClass F A B] (f : F) : GaloisConnection (NonUnitalStarSubalgebra.map f) (NonUnitalStarSubalgebra.comap f)
• NonUnitalStarSubalgebra.mem_comap 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] [NonUnitalNonAssocSemiring B] [Module R B] [Star B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [StarHomClass F A B] (S : NonUnitalStarSubalgebra R B) (f : F) (x : A) : x ∈ NonUnitalStarSubalgebra.comap f S ↔ f x ∈ S
• NonUnitalStarSubalgebra.mem_map 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] [NonUnitalNonAssocSemiring B] [Module R B] [Star B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [StarHomClass F A B] {S : NonUnitalStarSubalgebra R A} {f : F} {y : B} : y ∈ NonUnitalStarSubalgebra.map f S ↔ ∃ x ∈ S, f x = y
• NonUnitalStarSubalgebra.map_mono 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] [NonUnitalNonAssocSemiring B] [Module R B] [Star B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [StarHomClass F A B] {S₁ S₂ : NonUnitalStarSubalgebra R A} {f : F} : S₁ ≤ S₂ → NonUnitalStarSubalgebra.map f S₁ ≤ NonUnitalStarSubalgebra.map f S₂
• NonUnitalStarSubalgebra.map_le 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] [NonUnitalNonAssocSemiring B] [Module R B] [Star B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [StarHomClass F A B] {S : NonUnitalStarSubalgebra R A} {f : F} {U : NonUnitalStarSubalgebra R B} : NonUnitalStarSubalgebra.map f S ≤ U ↔ S ≤ NonUnitalStarSubalgebra.comap f U
• NonUnitalStarAlgHom.codRestrict 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] [NonUnitalNonAssocSemiring B] [Module R B] [Star B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [StarHomClass F A B] (f : F) (S : NonUnitalStarSubalgebra R B) (hf : ∀ (x : A), f x ∈ S) : A →⋆ₙₐ[R] ↥S
• NonUnitalStarAlgHom.rangeRestrict 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] [NonUnitalNonAssocSemiring B] [Module R B] [Star B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [StarHomClass F A B] (f : F) : A →⋆ₙₐ[R] ↥(NonUnitalStarAlgHom.range f)
• NonUnitalStarAlgHom.subtype_comp_codRestrict 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] [NonUnitalNonAssocSemiring B] [Module R B] [Star B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [StarHomClass F A B] (f : F) (S : NonUnitalStarSubalgebra R B) (hf : ∀ (x : A), f x ∈ S) : (NonUnitalStarSubalgebraClass.subtype S).comp (NonUnitalStarAlgHom.codRestrict f S hf) = ↑f
• NonUnitalStarAlgHom.coe_codRestrict 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] [NonUnitalNonAssocSemiring B] [Module R B] [Star B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [StarHomClass F A B] (f : F) (S : NonUnitalStarSubalgebra R B) (hf : ∀ (x : A), f x ∈ S) (x : A) : ↑((NonUnitalStarAlgHom.codRestrict f S hf) x) = f x
• NonUnitalStarAlgHom.injective_codRestrict 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] [NonUnitalNonAssocSemiring B] [Module R B] [Star B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [StarHomClass F A B] (f : F) (S : NonUnitalStarSubalgebra R B) (hf : ∀ (x : A), f x ∈ S) : Function.Injective ⇑(NonUnitalStarAlgHom.codRestrict f S hf) ↔ Function.Injective ⇑f
• NonUnitalStarSubalgebra.comap_center_le_center 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalSemiring A] [StarRing A] [Module R A] [NonUnitalSemiring B] [StarRing B] [Module R B] [IsScalarTower R A A] [SMulCommClass R A A] {F : Type u_1} [IsScalarTower R B B] [SMulCommClass R B B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [StarHomClass F A B] {f : F} (hf : Function.Injective ⇑f) : NonUnitalStarSubalgebra.comap f (NonUnitalStarSubalgebra.center R B) ≤ NonUnitalStarSubalgebra.center R A
• NonUnitalStarSubalgebra.map_center_le_center 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalSemiring A] [StarRing A] [Module R A] [NonUnitalSemiring B] [StarRing B] [Module R B] [IsScalarTower R A A] [SMulCommClass R A A] {F : Type u_1} [IsScalarTower R B B] [SMulCommClass R B B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [StarHomClass F A B] {f : F} (hf : Function.Surjective ⇑f) : NonUnitalStarSubalgebra.map f (NonUnitalStarSubalgebra.center R A) ≤ NonUnitalStarSubalgebra.center R B
• NonUnitalStarAlgHom.map_adjoin 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalSemiring A] [StarRing A] [Module R A] [NonUnitalSemiring B] [StarRing B] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [StarHomClass F A B] [StarRing R] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] [IsScalarTower R B B] [SMulCommClass R B B] [StarModule R B] (f : F) (s : Set A) : NonUnitalStarSubalgebra.map f (NonUnitalStarAlgebra.adjoin R s) = NonUnitalStarAlgebra.adjoin R (⇑f '' s)
• NonUnitalStarAlgHom.map_adjoin_singleton 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalSemiring A] [StarRing A] [Module R A] [NonUnitalSemiring B] [StarRing B] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [StarHomClass F A B] [StarRing R] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] [IsScalarTower R B B] [SMulCommClass R B B] [StarModule R B] (f : F) (x : A) : NonUnitalStarSubalgebra.map f (NonUnitalStarAlgebra.adjoin R {x}) = NonUnitalStarAlgebra.adjoin R {f x}
• NonUnitalStarAlgebra.range_eq_top 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [NonUnitalSemiring B] [StarRing B] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [StarHomClass F A B] [IsScalarTower R B B] [SMulCommClass R B B] [StarModule R B] (f : F) : NonUnitalStarAlgHom.range f = ⊤ ↔ Function.Surjective ⇑f
• NonUnitalStarAlgebra.map_top 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [NonUnitalSemiring B] [StarRing B] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [StarHomClass F A B] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] (f : F) : NonUnitalStarSubalgebra.map f ⊤ = NonUnitalStarAlgHom.range f
• NonUnitalStarAlgebra.map_iInf 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [NonUnitalSemiring B] [StarRing B] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [StarHomClass F A B] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] {ι : Sort u_1} [Nonempty ι] [IsScalarTower R B B] [SMulCommClass R B B] [StarModule R B] (f : F) (hf : Function.Injective ⇑f) (S : ι → NonUnitalStarSubalgebra R A) : NonUnitalStarSubalgebra.map f (⨅ i, S i) = ⨅ i, NonUnitalStarSubalgebra.map f (S i)
• NonUnitalStarAlgebra.map_sup 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [NonUnitalSemiring B] [StarRing B] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [StarHomClass F A B] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] [IsScalarTower R B B] [SMulCommClass R B B] [StarModule R B] (f : F) (S T : NonUnitalStarSubalgebra R A) : NonUnitalStarSubalgebra.map f (S ⊔ T) = NonUnitalStarSubalgebra.map f S ⊔ NonUnitalStarSubalgebra.map f T
• NonUnitalStarAlgebra.map_inf 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [NonUnitalSemiring B] [StarRing B] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [StarHomClass F A B] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] [IsScalarTower R B B] [SMulCommClass R B B] [StarModule R B] (f : F) (hf : Function.Injective ⇑f) (S T : NonUnitalStarSubalgebra R A) : NonUnitalStarSubalgebra.map f (S ⊓ T) = NonUnitalStarSubalgebra.map f S ⊓ NonUnitalStarSubalgebra.map f T
• NonUnitalStarAlgebra.comap_top 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [NonUnitalSemiring B] [StarRing B] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [StarHomClass F A B] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] [IsScalarTower R B B] [SMulCommClass R B B] [StarModule R B] (f : F) : NonUnitalStarSubalgebra.comap f ⊤ = ⊤
• NonUnitalStarAlgebra.map_bot 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [NonUnitalSemiring B] [StarRing B] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [StarHomClass F A B] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] [IsScalarTower R B B] [SMulCommClass R B B] [StarModule R B] (f : F) : NonUnitalStarSubalgebra.map f ⊥ = ⊥
• StarAlgEquiv.ofInjective' 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [Star A] [NonUnitalSemiring B] [Module R B] [Star B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [StarHomClass F A B] (f : F) (hf : Function.Injective ⇑f) : A ≃⋆ₐ[R] ↥(NonUnitalStarAlgHom.range f)
• StarAlgEquiv.ofLeftInverse' 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [Star A] [NonUnitalSemiring B] [Module R B] [Star B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [StarHomClass F A B] {g : B → A} {f : F} (h : Function.LeftInverse g ⇑f) : A ≃⋆ₐ[R] ↥(NonUnitalStarAlgHom.range f)
• StarAlgEquiv.ofInjective'_apply 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [Star A] [NonUnitalSemiring B] [Module R B] [Star B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [StarHomClass F A B] (f : F) (hf : Function.Injective ⇑f) (x : A) : ↑((StarAlgEquiv.ofInjective' f hf) x) = f x
• StarAlgEquiv.ofLeftInverse'_apply 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [Star A] [NonUnitalSemiring B] [Module R B] [Star B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [StarHomClass F A B] {g : B → A} {f : F} (h : Function.LeftInverse g ⇑f) (x : A) : ↑((StarAlgEquiv.ofLeftInverse' h) x) = f x
• StarAlgEquiv.ofLeftInverse'_symm_apply 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [Star A] [NonUnitalSemiring B] [Module R B] [Star B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [StarHomClass F A B] {g : B → A} {f : F} (h : Function.LeftInverse g ⇑f) (x : ↥(NonUnitalStarAlgHom.range f)) : (StarAlgEquiv.ofLeftInverse' h).symm x = g ↑x
• NonUnitalAlgHom.quasispectrum_apply_subset 📋 Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
  {F : Type u_3} {R : Type u_4} {A : Type u_5} {B : Type u_6} [CommSemiring R] [NonUnitalRing A] [NonUnitalRing B] [Module R A] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] (φ : F) (a : A) : quasispectrum R (φ a) ⊆ quasispectrum R a
• NonUnitalAlgHom.quasispectrum_apply_subset' 📋 Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
  {F : Type u_3} {R : Type u_4} (S : Type u_5) {A : Type u_6} {B : Type u_7} [CommSemiring R] [Semiring S] [NonUnitalRing A] [NonUnitalRing B] [Module R S] [Module S A] [Module R A] [Module S B] [Module R B] [IsScalarTower R S A] [IsScalarTower R S B] [FunLike F A B] [NonUnitalAlgHomClass F S A B] (φ : F) (a : A) : quasispectrum R (φ a) ⊆ quasispectrum R a
• DirectLimit.NonUnitalAlgebra.of 📋 Mathlib.Algebra.Colimit.DirectLimit
  {R : Type u_1} {ι : Type u_2} [Preorder ι] (G : ι → Type u_3) {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} (f : (x x_1 : ι) → (h : x ≤ x_1) → T h) [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [IsDirectedOrder ι] [CommSemiring R] [(i : ι) → NonUnitalNonAssocSemiring (G i)] [(i : ι) → DistribMulAction R (G i)] [∀ (i j : ι) (h : i ≤ j), NonUnitalAlgHomClass (T h) R (G i) (G j)] [Nonempty ι] (i : ι) : G i →ₙₐ[R] DirectLimit G f
• DirectLimit.NonUnitalAlgebra.lift 📋 Mathlib.Algebra.Colimit.DirectLimit
  {R : Type u_1} {ι : Type u_2} [Preorder ι] (G : ι → Type u_3) {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} (f : (x x_1 : ι) → (h : x ≤ x_1) → T h) [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [IsDirectedOrder ι] [CommSemiring R] [(i : ι) → NonUnitalNonAssocSemiring (G i)] [(i : ι) → DistribMulAction R (G i)] [∀ (i j : ι) (h : i ≤ j), NonUnitalAlgHomClass (T h) R (G i) (G j)] [Nonempty ι] (P : Type u_7) [NonUnitalNonAssocSemiring P] [DistribMulAction R P] (g : (i : ι) → G i →ₙₐ[R] P) (Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x) : DirectLimit G f →ₙₐ[R] P
• DirectLimit.NonUnitalAlgebra.lift_comp_of 📋 Mathlib.Algebra.Colimit.DirectLimit
  {R : Type u_1} {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [IsDirectedOrder ι] [CommSemiring R] [(i : ι) → NonUnitalNonAssocSemiring (G i)] [(i : ι) → DistribMulAction R (G i)] [∀ (i j : ι) (h : i ≤ j), NonUnitalAlgHomClass (T h) R (G i) (G j)] [Nonempty ι] (P : Type u_7) [NonUnitalNonAssocSemiring P] [DistribMulAction R P] (g : (i : ι) → G i →ₙₐ[R] P) (Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x) {i : ι} : (DirectLimit.NonUnitalAlgebra.lift G f P g Hg).comp (DirectLimit.NonUnitalAlgebra.of G f i) = g i
• DirectLimit.NonUnitalAlgebra.lift_toFun 📋 Mathlib.Algebra.Colimit.DirectLimit
  {R : Type u_1} {ι : Type u_2} [Preorder ι] (G : ι → Type u_3) {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} (f : (x x_1 : ι) → (h : x ≤ x_1) → T h) [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [IsDirectedOrder ι] [CommSemiring R] [(i : ι) → NonUnitalNonAssocSemiring (G i)] [(i : ι) → DistribMulAction R (G i)] [∀ (i j : ι) (h : i ≤ j), NonUnitalAlgHomClass (T h) R (G i) (G j)] [Nonempty ι] (P : Type u_7) [NonUnitalNonAssocSemiring P] [DistribMulAction R P] (g : (i : ι) → G i →ₙₐ[R] P) (Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x) (z : DirectLimit G f) : (DirectLimit.NonUnitalAlgebra.lift G f P g Hg) z = DirectLimit.lift f (fun x1 x2 => (g x1) x2) ⋯ z
• DirectLimit.NonUnitalAlgebra.of_f 📋 Mathlib.Algebra.Colimit.DirectLimit
  {R : Type u_1} {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [IsDirectedOrder ι] [CommSemiring R] [(i : ι) → NonUnitalNonAssocSemiring (G i)] [(i : ι) → DistribMulAction R (G i)] [∀ (i j : ι) (h : i ≤ j), NonUnitalAlgHomClass (T h) R (G i) (G j)] [Nonempty ι] {i j : ι} (hij : i ≤ j) (x : G i) : (DirectLimit.NonUnitalAlgebra.of G f j) ((f i j hij) x) = (DirectLimit.NonUnitalAlgebra.of G f i) x
• DirectLimit.NonUnitalAlgebra.lift_of 📋 Mathlib.Algebra.Colimit.DirectLimit
  {R : Type u_1} {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [IsDirectedOrder ι] [CommSemiring R] [(i : ι) → NonUnitalNonAssocSemiring (G i)] [(i : ι) → DistribMulAction R (G i)] [∀ (i j : ι) (h : i ≤ j), NonUnitalAlgHomClass (T h) R (G i) (G j)] [Nonempty ι] (P : Type u_7) [NonUnitalNonAssocSemiring P] [DistribMulAction R P] (g : (i : ι) → G i →ₙₐ[R] P) (Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x) (i : ι) (x : G i) : (DirectLimit.NonUnitalAlgebra.lift G f P g Hg) ((DirectLimit.NonUnitalAlgebra.of G f i) x) = (g i) x
• DirectLimit.NonUnitalAlgebra.hom_ext 📋 Mathlib.Algebra.Colimit.DirectLimit
  {R : Type u_1} {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [IsDirectedOrder ι] [CommSemiring R] [(i : ι) → NonUnitalNonAssocSemiring (G i)] [(i : ι) → DistribMulAction R (G i)] [∀ (i j : ι) (h : i ≤ j), NonUnitalAlgHomClass (T h) R (G i) (G j)] [Nonempty ι] (P : Type u_7) [NonUnitalNonAssocSemiring P] [DistribMulAction R P] {g₁ g₂ : DirectLimit G f →ₙₐ[R] P} (h : ∀ (i : ι), g₁.comp (DirectLimit.NonUnitalAlgebra.of G f i) = g₂.comp (DirectLimit.NonUnitalAlgebra.of G f i)) : g₁ = g₂
• DirectLimit.NonUnitalAlgebra.hom_ext_iff 📋 Mathlib.Algebra.Colimit.DirectLimit
  {R : Type u_1} {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [IsDirectedOrder ι] [CommSemiring R] [(i : ι) → NonUnitalNonAssocSemiring (G i)] [(i : ι) → DistribMulAction R (G i)] [∀ (i j : ι) (h : i ≤ j), NonUnitalAlgHomClass (T h) R (G i) (G j)] [Nonempty ι] {P : Type u_7} [NonUnitalNonAssocSemiring P] [DistribMulAction R P] {g₁ g₂ : DirectLimit G f →ₙₐ[R] P} : g₁ = g₂ ↔ ∀ (i : ι), g₁.comp (DirectLimit.NonUnitalAlgebra.of G f i) = g₂.comp (DirectLimit.NonUnitalAlgebra.of G f i)
• NormedAlgebra.induced 📋 Mathlib.Analysis.Normed.Module.Basic
  {F : Type u_6} (𝕜 : Type u_7) (R : Type u_8) (S : Type u_9) [NormedField 𝕜] [Ring R] [Algebra 𝕜 R] [SeminormedRing S] [NormedAlgebra 𝕜 S] [FunLike F R S] [NonUnitalAlgHomClass F 𝕜 R S] (f : F) : NormedAlgebra 𝕜 R
• NonUnitalStarAlgHomClass.map_cfcₙ 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
  {F : Type u_1} {R : Type u_2} {S : Type u_3} {A : Type u_4} {B : Type u_5} {p : A → Prop} {q : B → Prop} [CommSemiring R] [Nontrivial R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [CommRing S] [Algebra R S] [NonUnitalRing A] [StarRing A] [TopologicalSpace A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [NonUnitalRing B] [StarRing B] [TopologicalSpace B] [Module R B] [IsScalarTower R B B] [SMulCommClass R B B] [Module S A] [Module S B] [IsScalarTower R S A] [IsScalarTower R S B] [NonUnitalContinuousFunctionalCalculus R A p] [NonUnitalContinuousFunctionalCalculus R B q] [ContinuousMapZero.UniqueHom R B] [FunLike F A B] [NonUnitalAlgHomClass F S A B] [StarHomClass F A B] (φ : F) (f : R → R) (a : A) (hf : ContinuousOn f (quasispectrum R a) := by cfc_cont_tac) (hf₀ : f 0 = 0 := by cfc_zero_tac) (hφ : Continuous ⇑φ := by fun_prop) (ha : p a := by cfc_tac) (hφa : q (φ a) := by cfc_tac) : φ (cfcₙ f a) = cfcₙ f (φ a)
• WeakDual.CharacterSpace.instNonUnitalAlgHomClass 📋 Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace
  {𝕜 : Type u_1} {A : Type u_2} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [NonUnitalNonAssocSemiring A] [TopologicalSpace A] [Module 𝕜 A] : NonUnitalAlgHomClass (↑(WeakDual.characterSpace 𝕜 A)) 𝕜 A 𝕜
• NonUnitalStarAlgHom.norm_apply_le 📋 Mathlib.Analysis.CStarAlgebra.Spectrum
  {F : Type u_1} {A : Type u_2} {B : Type u_3} [NonUnitalCStarAlgebra A] [NonUnitalCStarAlgebra B] [FunLike F A B] [NonUnitalAlgHomClass F ℂ A B] [StarHomClass F A B] (φ : F) (a : A) : ‖φ a‖ ≤ ‖a‖
• NonUnitalStarAlgHom.nnnorm_apply_le 📋 Mathlib.Analysis.CStarAlgebra.Spectrum
  {F : Type u_1} {A : Type u_2} {B : Type u_3} [NonUnitalCStarAlgebra A] [NonUnitalCStarAlgebra B] [FunLike F A B] [NonUnitalAlgHomClass F ℂ A B] [StarHomClass F A B] (φ : F) (a : A) : ‖φ a‖₊ ≤ ‖a‖₊
• NonUnitalStarAlgHom.instContinuousLinearMapClassComplex 📋 Mathlib.Analysis.CStarAlgebra.Spectrum
  {F : Type u_1} {A : Type u_2} {B : Type u_3} [NonUnitalCStarAlgebra A] [NonUnitalCStarAlgebra B] [FunLike F A B] [NonUnitalAlgHomClass F ℂ A B] [StarHomClass F A B] : ContinuousLinearMapClass F ℂ A B
• NonUnitalStarAlgHom.norm_map 📋 Mathlib.Analysis.CStarAlgebra.Hom
  {F : Type u_1} {A : Type u_2} {B : Type u_3} [NonUnitalCStarAlgebra A] [NonUnitalCStarAlgebra B] [FunLike F A B] [NonUnitalAlgHomClass F ℂ A B] [StarHomClass F A B] (φ : F) (hφ : Function.Injective ⇑φ) (a : A) : ‖φ a‖ = ‖a‖
• NonUnitalStarAlgHom.isometry 📋 Mathlib.Analysis.CStarAlgebra.Hom
  {F : Type u_1} {A : Type u_2} {B : Type u_3} [NonUnitalCStarAlgebra A] [NonUnitalCStarAlgebra B] [FunLike F A B] [NonUnitalAlgHomClass F ℂ A B] [StarHomClass F A B] (φ : F) (hφ : Function.Injective ⇑φ) : Isometry ⇑φ
• NonUnitalStarAlgHom.nnnorm_map 📋 Mathlib.Analysis.CStarAlgebra.Hom
  {F : Type u_1} {A : Type u_2} {B : Type u_3} [NonUnitalCStarAlgebra A] [NonUnitalCStarAlgebra B] [FunLike F A B] [NonUnitalAlgHomClass F ℂ A B] [StarHomClass F A B] (φ : F) (hφ : Function.Injective ⇑φ) (a : A) : ‖φ a‖₊ = ‖a‖₊
• NonUnitalStarAlgHom.map_le_map_iff 📋 Mathlib.Analysis.CStarAlgebra.Hom
  {F : Type u_1} {A : Type u_2} {B : Type u_3} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] [NonUnitalCStarAlgebra B] [PartialOrder B] [StarOrderedRing B] [FunLike F A B] [NonUnitalAlgHomClass F ℂ A B] [StarHomClass F A B] (f : F) (hf : Function.Injective ⇑f) {x y : A} : f x ≤ f y ↔ x ≤ y
• NonUnitalStarAlgHom.map_lt_map_iff 📋 Mathlib.Analysis.CStarAlgebra.Hom
  {F : Type u_1} {A : Type u_2} {B : Type u_3} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] [NonUnitalCStarAlgebra B] [PartialOrder B] [StarOrderedRing B] [FunLike F A B] [NonUnitalAlgHomClass F ℂ A B] [StarHomClass F A B] (f : F) (hf : Function.Injective ⇑f) {x y : A} : f x < f y ↔ x < y
• IsSelfAdjoint.map_quasispectrum_real 📋 Mathlib.Analysis.CStarAlgebra.Hom
  {F : Type u_1} {A : Type u_2} {B : Type u_3} [NonUnitalCStarAlgebra A] [NonUnitalCStarAlgebra B] [FunLike F A B] [NonUnitalAlgHomClass F ℂ A B] [StarHomClass F A B] {a : A} (ha : IsSelfAdjoint a) (φ : F) (hφ : Function.Injective ⇑φ) : quasispectrum ℝ (φ a) = quasispectrum ℝ a
• NonUnitalStarAlgHomClass.instCompletelyPositiveMapClass 📋 Mathlib.Analysis.CStarAlgebra.CompletelyPositiveMap
  {F : Type u_1} {A₁ : Type u_2} {A₂ : Type u_3} [NonUnitalCStarAlgebra A₁] [NonUnitalCStarAlgebra A₂] [PartialOrder A₁] [PartialOrder A₂] [StarOrderedRing A₁] [StarOrderedRing A₂] [FunLike F A₁ A₂] [NonUnitalAlgHomClass F ℂ A₁ A₂] [StarHomClass F A₁ A₂] : CompletelyPositiveMapClass F A₁ A₂

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. 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.

5. You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

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. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 9f11169 serving mathlib revision 69fae59